dsimp [boundLeft, List.predHead] at hays
α : Type u
r : α → α → Prop
β : α → Type v
inst✝ : Trans r r r
xs : KVChain (flip r) β
a : α
b : β a
ys : KVChain r β
hays : boundLeft a ys
a₁ : α
x✝³ : β a₁
x✝² : KVChain (flip r) β
x✝¹ : boundLeft a₁ x✝²
x✝ : hingeable x✝² (KVChain.cons a b ys hays) → hingeable x✝² ys
⊢ r a₁ a →
    match ys.toList with
    | [] => True
    | a :: tail => r a₁ a.fst
α : 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
⊢ r a₁ a →
    match ys.toList with
    | [] => True
    | a :: tail => r a₁ a.fst