simp [reverse, reverse_append]
case sandwich
α : Type
xs✝ : List α
x : α
xs : List α
hxs : Palindrome xs
ih : Palindrome (reverse xs)
⊢ Palindrome (reverse ([x] ++ xs ++ [x]))
case sandwich
α : Type
xs✝ : List α
x : α
xs : List α
hxs : Palindrome xs
ih : Palindrome (reverse xs)
⊢ Palindrome (x :: (reverse xs ++ [x]))