case snd_Ascending => exact hhook.snd_Ascending.tail
α : 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)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ Ascending r bs
no goals