--- /dev/null
+record empty : Type \def {}.
+
+record pippo : Type \def
+{
+a: Set ;
+b: a \to Prop;
+c: \forall x:a.(b x) \to a \to Type
+}.
+
+record pluto (A, B:Set) : Type \def {
+d: A \to B \to Prop;
+e: \forall y:A.\forall z:B. (d y z) \to A \to B;
+mario: \forall y:A.\forall z:B. \forall h:(d y z). \forall i : B \to Prop.
+ i (e y z h y)
+}.
+
+record paperino: Prop \def {
+ paolo : Type;
+ pippo : paolo \to paolo;
+ piero : True
+}.
\ No newline at end of file