1 record empty : Type \def {}.
3 inductive True : Prop \def I: True.
5 record pippo : Type \def
9 c: \forall x:a.(b x) \to a \to Type
12 record pluto (A, B:Set) : Type \def {
14 e: \forall y:A.\forall z:B. (d y z) \to A \to B;
15 mario: \forall y:A.\forall z:B. \forall h:(d y z). \forall i : B \to Prop.
19 record paperino: Prop \def {
21 pippo : paolo \to paolo;