intro hass
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
a : α
as : List α
h_ind : Ascending r (as ++ bs) → List.forAllRel r as bs
⊢ Ascending r (a :: (as ++ bs)) → forAll (r a) bs ∧ List.forAllRel r as bs
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
a : α
as : List α
h_ind : Ascending r (as ++ bs) → List.forAllRel r as bs
hass : Ascending r (a :: (as ++ bs))
⊢ forAll (r a) bs ∧ List.forAllRel r as bs