(* *)
(**************************************************************************)
+(* STATO: NON COMPILA: attendo che l'oggetto "pippo" venga accettato *)
+
set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/coa_defs".
include "iff.ma".
inductive pippo : Prop \def
| Pippo: let x \def zero in zero = x \to pippo.
-
\ No newline at end of file
+