simp
α : Type
hd : α
tl : List α
ih : tl.reverse ∈ exp α tl.length
⊢ (hd :: tl).reverse ∈ exp α (hd :: tl).length
α : Type
hd : α
tl : List α
ih : tl.reverse ∈ exp α tl.length
⊢ tl.reverse ++ [hd] ∈ exp α (tl.length + 1)