(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/LOGIC/datatypes_defs/Proof".
+
(* PROOFS
- Naming policy:
- proofs: p q r s
*)
-include "preamble.ma".
+include "preamble0.ma".
inductive Proof: Type \def
| lref: Nat \to Proof (* projection *)