induction s
α : Type
s : Str α
⊢ List.reverse s ∈ exp α (List.length s)
case nil
α : Type
⊢ [].reverse ∈ exp α [].length

case cons
α : Type
head✝ : α
tail✝ : List α
tail_ih✝ : tail✝.reverse ∈ exp α tail✝.length
⊢ (head✝ :: tail✝).reverse ∈ exp α (head✝ :: tail✝).length