dsimp [predHead] at *
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✝)
⊢ r head✝¹ head✝
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✝¹ : r₁ head✝¹ b
a✝ : r₂ b head✝
⊢ r head✝¹ head✝