∀ {α : Type u_1} {motive : (a : List α) → a.Palindrome → Prop},
  motive [] ⋯ →
    (∀ (x : α), motive [x] ⋯) →
      (∀ (x : α) {l : List α} (a : l.Palindrome), motive l a → motive (x :: (l ++ [x])) ⋯) →
        ∀ {a : List α} (t : a.Palindrome), motive a t