induction h1
α : Type
s : Str α
n : ℕ
h1 : s ∈ exp α n
⊢ List.length s = n
case zero
α : Type
s : Str α
n : ℕ
⊢ [].length = 0

case succ
α : Type
s : Str α
n n✝ : ℕ
a✝¹ : α
s✝ : Str α
a✝ : s✝ ∈ exp α n✝
a_ih✝ : List.length s✝ = n✝
⊢ List.length (s✝ ++ [a✝¹]) = n✝ + 1