Proofs have types too

Naming a rule makes its derivations values. The predicate’s name also names their type.

:: Succ(P: nat) checks the constructor payload. P : nat(_) captures a proof; P: nat in the head declares its type. Aliases and nested types work too: [nat?].

Contracts do not cast JSON into proofs. Derive a tuple to build a proof; constructor terms are matches. Module wiring preserves the producer's identity.