[Typer] Typer and proofs

Je ne comprends pas comment définir en Typer:

Inductive even: nat -> Prop := % Premier axiome | even0 : even 0 % Deuxième axiome | evenS : forall x:nat, even x -> even (S (S x)).

j'ai quelque chose comme:

even : Type; even = typecons (even (n : Nat)) (even0 (Eq (t := Nat) zero n)) (evenS ();

mais je ne comprends ce que `forall x:nat, even x -> even (S (S x))` fait en temps que tel.