exact h_ind ∘ Ascending.tail
α : Type u
r : α → α → Prop
bs : List α
head✝ : α
tail✝ : List α
h_ind : Ascending r (tail✝ ++ bs) → Ascending r bs
⊢ Ascending r (head✝ :: tail✝ ++ bs) → Ascending r bs
no goals