1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8

-- https://lean-lang.org/documentation/examples/palindromes/

inductive Palindrome : List Nat → Prop where
  | nil      : Palindrome []
  | single   : (a : Nat) → Palindrome [a]
  | sandwich : (a : Nat) → Palindrome as → Palindrome ([a] ++ as ++ [a])

#eval (Palindrome [3, 3])