have hhead : bs.forAll (r a) := h.left
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
a : α
as : List α
h_ind : List.forAllRel r as bs → Ascending r as → Ascending r bs → Ascending r (as ++ bs)
h : forAll (r a) bs ∧ List.forAllRel r as bs
hass : Ascending r (a :: as)
hbs : Ascending r bs
htail : Ascending r (as ++ bs)
⊢ Ascending r (a :: (as ++ bs))
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
a : α
as : List α
h_ind : List.forAllRel r as bs → Ascending r as → Ascending r bs → Ascending r (as ++ bs)
h : forAll (r a) bs ∧ List.forAllRel r as bs
hass : Ascending r (a :: as)
hbs : Ascending r bs
htail : Ascending r (as ++ bs)
hhead : forAll (r a) bs
⊢ Ascending r (a :: (as ++ bs))