case snd_Ascending =>
  exact hhook.snd_Ascending.of_implies himp
α : Type u_1
r r₁ : α → α → Prop
himp : ∀ (a b : α), r a b → r₁ a b
as bs : List α
hhook : HookedAscending r as bs
⊢ Ascending r₁ bs
no goals