no goals
α : Type u_1
β : Type u_2
γ : Type ?u.1154
δ : Type ?u.1157
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
H : ∀ (a : α) (b : β), R a b → S a b
l₁ : List α
l₂ : List β
h : Forall₂ R l₁ l₂
⊢ Forall₂ S l₁ l₂
induction h <;> constructor <;> solve_by_elim