exact trans ‹r₁ _ b› ‹r₂ b _›
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✝
no goals