simp
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)
a b : F
bs : List F
ih : motive (b :: bs)
⊢ b :: bs ≠ []
no goals