first | apply EmptyStringPrefix | apply CharPrefix | apply PrefixAppend
case notP_2
V_N V_T : Type
R : V_N → PE V_N V_T
xs : List V_T
e✝ : PE V_N V_T
n✝ : ℕ
a✝ : Interpretation V_N V_T R (e✝, xs) (n✝, none)
ih : ∀ m < n✝ + 1, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, xs) (m, some []) → [].IsPrefix xs
⊢ [].IsPrefix xs
no goals