simp
α : Type
s✝ : Str α
n m : ℕ
a : α
s : Str α
ih_1 : s ∈ exp α m
ih_2 : List.length s = m
⊢ List.length (s ++ [a]) = m + 1
α : Type
s✝ : Str α
n m : ℕ
a : α
s : Str α
ih_1 : s ∈ exp α m
ih_2 : List.length s = m
⊢ List.length s = m