cases as <;> cases cs <;> intros <;> try {intros; exact True.intro}
α : 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 γ
⊢ predHead (fun a => r₁ a b) as → predHead (r₂ b) cs → relHead r as cs
case cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
b : β
head✝¹ : α
tail✝¹ : List α
head✝ : γ
tail✝ : List γ
a✝¹ : predHead (fun a => r₁ a b) (head✝¹ :: tail✝¹)
a✝ : predHead (r₂ b) (head✝ :: tail✝)
⊢ relHead r (head✝¹ :: tail✝¹) (head✝ :: tail✝)