1 %% test per matita.lang
3 set "baseuri" "cic:/matita/tests/".
9 inductive pippo : Type \def
14 definition pollo : Set \to Set \def
17 inductive paolo : Prop \def t:paolo.
19 theorem comeno : \forall p:pippo.pippo.
23 definition f : pippo \to paolo \def
28 | (c z) \Rightarrow t ].
30 record w : Type \def {