induction as with
| nil => exact hnil;
| cons a as ih => cases as with
  | nil => exact hsingle a;
  | cons b bs => exact hcons a (b :: bs) (by simp) ih;
F : Type u
inst✝ : LogicalConnective F
p q : F
motive : List F → Prop
hnil : motive []
hsingle : ∀ (a : F), motive [a]
hcons : ∀ (a : F) (as : List F), as ≠ [] → motive as → motive (a :: as)
as : List F
⊢ motive as
no goals