X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fcontribs%2FLOGIC%2Fdatatypes%2FProof.ma;fp=matita%2Fcontribs%2FLOGIC%2Fdatatypes%2FProof.ma;h=357b044f5a448494fed4a9de7a50d612993d9ac0;hb=78d54ce55b983b74fa6cce3cb085f207215c5cac;hp=8643eb826518b7a44ca534c1e2a563f082180005;hpb=22a4eca2fd746d689d491140d43cfd5ffe31f19e;p=helm.git

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