induction as <;> simp
α✝ : Type ?u.5956
β✝ : Type ?u.5959
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
as : List α
b : β
cs : List γ
⊢ forAll (fun x => r₁ x b) as → forAll (r₂ b) cs → List.forAllRel r as cs
case cons
α✝ : Type ?u.5956
β✝ : Type ?u.5959
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
b : β
cs : List γ
head✝ : α
tail✝ : List α
tail_ih✝ : forAll (fun x => r₁ x b) tail✝ → forAll (r₂ b) cs → List.forAllRel r tail✝ cs
⊢ forAll (fun x => r₁ x b) (head✝ :: tail✝) → forAll (r₂ b) cs → forAll (r head✝) cs ∧ List.forAllRel r tail✝ cs