X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLOGIC%2Fdatatypes%2FProof.ma;h=357b044f5a448494fed4a9de7a50d612993d9ac0;hb=5e736134ceab076b4e963d535f380ffa796a5d19;hp=8643eb826518b7a44ca534c1e2a563f082180005;hpb=e0b576827e1d1dd243f304e68cda6b0c7cc21978;p=helm.git

diff --git a/helm/software/matita/contribs/LOGIC/datatypes/Proof.ma b/helm/software/matita/contribs/LOGIC/datatypes/Proof.ma
index 8643eb826..357b044f5 100644
--- a/helm/software/matita/contribs/LOGIC/datatypes/Proof.ma
+++ b/helm/software/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      *)
 .