case a
α : Type u_1
β : Type ?u.1074
l✝ l : List α
⊢ reverse (l ++ reverse l) = l ++ reverse l
α : Type u_1
β : Type ?u.1074
l✝ l : List α
⊢ Palindrome (l ++ reverse l)
apply of_reverse_eq
no goals
case a
α : Type u_1
β : Type ?u.1074
l✝ l : List α
⊢ reverse (l ++ reverse l) = l ++ reverse l
rw [reverse_append, reverse_reverse]