intro hab hba hhook
α : Type u_1
r : α → α → Prop
inst✝² : Trans r r r
eqv : α → α → Prop
inst✝¹ : Trans eqv r r
inst✝ : Trans r eqv r
a b : α
as bs : List α
⊢ eqv a b → eqv b a → HookedAscending r as (b :: bs) → HookedAscending r (a :: as) bs
α : Type u_1
r : α → α → Prop
inst✝² : Trans r r r
eqv : α → α → Prop
inst✝¹ : Trans eqv r r
inst✝ : Trans r eqv r
a b : α
as bs : List α
hab : eqv a b
hba : eqv b a
hhook : HookedAscending r as (b :: bs)
⊢ HookedAscending r (a :: as) bs