obtain s1 := rev_str_mem_exp_str_len s.reverse
α : Type
s : Str α
⊢ s ∈ exp α (List.length s)
α : Type
s : Str α
s1 : (List.reverse s).reverse ∈ exp α (List.reverse s).length
⊢ s ∈ exp α (List.length s)