α : Type u_1
β : Type u_2
γ : Type ?u.140328
δ : Type ?u.140331
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₁ : R a✝ b✝
h₂ : Forall₂ R l₁✝ l₂✝
⊢ Forall₂ R (reverse l₁✝ ++ [a✝]) (reverse l₂✝ ++ [b✝])
α : Type u_1
β : Type u_2
γ : Type ?u.140328
δ : Type ?u.140331
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₁ : R a✝ b✝
h₂ : Forall₂ R l₁✝ l₂✝
⊢ Forall₂ R (reverse (a✝ :: l₁✝)) (reverse (b✝ :: l₂✝))
simp only [reverse_cons]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.140328
δ : Type ?u.140331
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
a✝ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
h₁ : R a✝ b✝
h₂ : Forall₂ R l₁✝ l₂✝
⊢ Forall₂ R (reverse l₁✝ ++ [a✝]) (reverse l₂✝ ++ [b✝])
exact rel_append (rel_reverse h₂) (Forall₂.cons h₁ Forall₂.nil)