feat(data/list/palindrome): define palindromes (#3729)
This introduces an inductive type `palindrome`, with conversions to and from the proposition `reverse l = l`.
Review of this PR indicates two things: (1) maybe the name `is_palindrome` is better, especially if we define the subtype of palindromic lists; (2) maybe defining palindrome by `reverse l = l` is simpler. We note these for future development.
Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
