Theorem: List.forAllRel_reverse_right (Algdata/Data/List/Prop.lean)

State before:
α : Type u_1
β : Type u_2
r : α → β → Prop
as : List α
bs : List β
⊢ List.forAllRel r as (reverse bs) = List.forAllRel r as bs
Tactic:
rw [←forAllRel_flip, ←forAllRel_flip (r:=r)]
State after:
α : Type u_1
β : Type u_2
r : α → β → Prop
as : List α
bs : List β
⊢ List.forAllRel (flip r) (reverse bs) as = List.forAllRel (flip r) bs as

State before:
α : Type u_1
β : Type u_2
r : α → β → Prop
as : List α
bs : List β
⊢ List.forAllRel (flip r) (reverse bs) as = List.forAllRel (flip r) bs as
Tactic:
exact forAllRel_reverse_left
State after:
no goals