induction hxs with
| nil                  => exact Palindrome.nil
| single x             => exact Palindrome.single x
| sandwich x xs hxs ih =>
  { simp [reverse, reverse_append]
    exact Palindrome.sandwich _ _ ih }
α : Type
xs : List α
hxs : Palindrome xs
⊢ Palindrome (reverse xs)
no goals