proof by "introduction" (impi) implemented in full

[helm.git] / matita / contribs / LOGIC / datatypes / Proof.ma

diff --git a/matita/contribs/LOGIC/datatypes/Proof.ma b/matita/contribs/LOGIC/datatypes/Proof.ma
index 8643eb826518b7a44ca534c1e2a563f082180005..357b044f5a448494fed4a9de7a50d612993d9ac0 100644 (file)
--- a/matita/contribs/LOGIC/datatypes/Proof.ma
+++ b/matita/contribs/LOGIC/datatypes/Proof.ma
@@ -22,12 +22,10 @@ set "baseuri" "cic:/matita/LOGIC/datatypes/Proof".
 include "preamble.ma".
 
 inductive Proof: Type \def
-   | lref: Nat \to Proof
-   | parx: Nat \to Proof
-   | impw: Proof \to Proof
-   | impi: Proof \to Proof
-   | impe: Proof \to Proof
-(*   
-   | impe: Proof \to Proof \to Proof \to Proof
-*)
+   | lref: Nat \to Proof                       (* projection         *)
+   | parx: Nat \to Proof                       (*                    *)
+   | impw: Proof \to Proof                     (* weakening          *)
+   | impr: Proof \to Proof                     (* right introduction *)
+   | impi: Proof \to Proof \to Proof \to Proof (* left introduction  *)
+   | scut: Proof \to Proof \to Proof           (* symmetric cut      *)
 .