In CoQ, cosa significa avere un tipo induttivo in cui il lato destro di ":" è prop?

Question

Sono nuovo a CoQ e la mia comprensione (piuttosto limitata) è che i tipi induttivi sono come i dati algebrici di Haskell, quindi c'è un costruttore data T = A a con alcuni argomenti e il risultato A a è un T: in particolare a T, quindi capisco cose come questa:

Inductive List := Nil : List | Cons : nat -> List -> List.

dove si applica un costruttore e ottieni un elenco, che definisce quali elenchi (al contrario di qualcos'altro) sono.

Quindi, come funziona esattamente che posso definire un tipo induttivo come questo:

Inductive Person := Name : nat -> Person.
Inductive Knight : Person -> Prop := Knight_ : ∀(A:Person), Knight A.
Inductive Knave : Person -> Prop := Knave_ : ∀A, Knave A.

dove il tipo induttivo ha prop (o Person -> Prop?) Sul lato destro di esso? Ciò dovrebbe rappresentare "A Is A Knight" e "A is a Knave" nei puzzle di cavalieri e marittimi. Penso che questo sia un modo per codificare l'idea, ma questo è un po 'confuso, e non sono riuscito a trovare una spiegazione di questo. Alcuni posti in effetti introducono tipi induttivi come simili ai dati di Haskell, ma chiaramente non è tutto.