How to choose between prop and type?

Stream: general

[Erika Su]

Consider

inductive Palindrome : List α → /- Prop or Type  -/ where
  | nil : Palindrome []
  | single : (a : α) → Palindrome [a]
  | sandwich : (a : α) → Palindrome as → Palindrome ([a] ++ as ++ [a])

Prop is useful for proving, but Type is also useful as it provides a "View" of List
(I learned this concept in type driven development in idris).
If it's only about proving then prop should be used. But it's also possible i need to give a computable function using view.
I don't think define two version (Prop and Type) of this inductive type is good practice, but i am also worried that using the latter will affect performance of the program when only type check is needed.
What's the best practice?