case cons hd tl ih =>
  apply Exists.elim ih
  intro n a1
  apply Exists.intro (n + 1)
  simp
  exact exp.succ n hd tl.reverse a1
α : Type
hd : α
tl : List α
ih : ∃ n, tl.reverse ∈ exp α n
⊢ ∃ n, (hd :: tl).reverse ∈ exp α n
no goals