apply PrefixAppend
case star_repetition
V_N V_T : Type
R : V_N → PE V_N V_T
e✝ : PE V_N V_T
xs_1✝ xs_2✝ ys✝ : List V_T
n1✝ n2✝ : ℕ
a✝¹ : Interpretation V_N V_T R (e✝, xs_1✝ ++ xs_2✝ ++ ys✝) (n1✝, some xs_1✝)
a✝ : Interpretation V_N V_T R (e✝.star, xs_2✝ ++ ys✝) (n2✝, some xs_2✝)
ih :
  ∀ m < n1✝ + n2✝ + 1,
    ∀ (e : PE V_N V_T),
      Interpretation V_N V_T R (e, xs_1✝ ++ xs_2✝ ++ ys✝) (m, some (xs_1✝ ++ xs_2✝)) →
        (xs_1✝ ++ xs_2✝).IsPrefix (xs_1✝ ++ xs_2✝ ++ ys✝)
⊢ (xs_1✝ ++ xs_2✝).IsPrefix (xs_1✝ ++ xs_2✝ ++ ys✝)
no goals