exact trans (t:=r) h hays
α : Type u
r : α → α → Prop
β : α → Type v
inst✝ : Trans r r r
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hays✝ :
  match ys.toList with
  | [] => True
  | a_1 :: tail => r a a_1.fst
a₁ : α
x✝³ : β a₁
x✝² : KVChain (flip r) β
x✝¹ : boundLeft a₁ x✝²
x✝ : hingeable x✝² (KVChain.cons a b ys hays✝) → hingeable x✝² ys
head✝ : Sigma β
tail✝ : List (Sigma β)
hays :
  match head✝ :: tail✝ with
  | [] => True
  | a_1 :: tail => r a a_1.fst
hys : ys.toList = head✝ :: tail✝
h : r a₁ a
⊢ match head✝ :: tail✝ with
  | [] => True
  | a :: tail => r a₁ a.fst
no goals