1 record empty : Type \def {}.
3 record pippo : Type \def
7 c: \forall x:a.(b x) \to a \to Type
10 record pluto (A, B:Set) : Type \def {
12 e: \forall y:A.\forall z:B. (d y z) \to A \to B;
13 mario: \forall y:A.\forall z:B. \forall h:(d y z). \forall i : B \to Prop.
17 record paperino: Prop \def {
19 pippo : paolo \to paolo;