α : Type u_1
β : Type u_2
γ : Type ?u.142594
δ : Type ?u.142597
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂ : List β
h : Forall₂ R (reverse l₁) (reverse l₂)
⊢ Forall₂ R (reverse (reverse l₁)) (reverse (reverse l₂))
α : Type u_1
β : Type u_2
γ : Type ?u.142594
δ : Type ?u.142597
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂ : List β
h : Forall₂ R (reverse l₁) (reverse l₂)
⊢ Forall₂ R l₁ l₂
rw [← reverse_reverse l₁, ← reverse_reverse l₂]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.142594
δ : Type ?u.142597
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
l₁ : List α
l₂ : List β
h : Forall₂ R (reverse l₁) (reverse l₂)
⊢ Forall₂ R (reverse (reverse l₁)) (reverse (reverse l₂))
exact rel_reverse h