exact hsingle a
case cons.nil
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 : F
ih : motive []
⊢ motive [a]
no goals