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