cases as <;> simp
α : Type u_1
r : α → α → Prop
as bs : List α
⊢ HookedAscending r as bs → Ascending r (reverseAux as bs)
case nil
α : Type u_1
r : α → α → Prop
bs : List α
⊢ HookedAscending r [] bs → Ascending r bs

case cons
α : Type u_1
r : α → α → Prop
bs : List α
head✝ : α
tail✝ : List α
⊢ HookedAscending r (head✝ :: tail✝) bs → Ascending r (reverseAux tail✝ (head✝ :: bs))