1 set "baseuri" "cic:/matita/tests/record/".
3 record empty : Type \def {}.
5 inductive True : Prop \def I: True.
7 record pippo : Type \def
11 c: \forall x:a.(b x) \to a \to Type
14 record pluto (A, B:Set) : Type \def {
16 e: \forall y:A.\forall z:B. (d y z) \to A \to B;
17 mario: \forall y:A.\forall z:B. \forall h:(d y z). \forall i : B \to Prop.
21 record paperino: Prop \def {
23 pippo : paolo \to paolo;