case nil => exact absurd rfl hbs
α✝ : Type ?u.8039
β✝ : Type ?u.8042
r✝ : α✝ → β✝ → Prop
α : Type u_1
β : Type u_2
γ : Type u_3
r₁ : α → β → Prop
r₂ : β → γ → Prop
r : α → γ → Prop
inst✝ : Trans r₁ r₂ r
as : List α
cs : List γ
hbs : [] ≠ []
hab : List.forAllRel r₁ as []
hbc : List.forAllRel r₂ [] cs
⊢ List.forAllRel r as cs
no goals