apply CharPrefix
case terminal_success
V_N V_T : Type
R : V_N → PE V_N V_T
a✝ : V_T
xs✝ : List V_T
ih : ∀ m < 1, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, a✝ :: xs✝) (m, some [a✝]) → [a✝].IsPrefix (a✝ :: xs✝)
⊢ [a✝].IsPrefix (a✝ :: xs✝)
no goals