simp
α : Type
hd : α
tl : List α
ih : ∃ n, tl.reverse ∈ exp α n
n : ℕ
a1 : tl.reverse ∈ exp α n
⊢ (hd :: tl).reverse ∈ exp α (n + 1)
α : Type
hd : α
tl : List α
ih : ∃ n, tl.reverse ∈ exp α n
n : ℕ
a1 : tl.reverse ∈ exp α n
⊢ tl.reverse ++ [hd] ∈ exp α (n + 1)