axiomatization of acc_if

[helm.git] / matita / matita / lib / lambda / cube.ma

diff --git a/matita/matita/lib/lambda/cube.ma b/matita/matita/lib/lambda/cube.ma
index 9ddaed35ccb0b6a0dd019ee65daa79cdbf179514..8ac3d978c74f5e6a889cdcc155916c19cf084380 100644 (file)
--- a/matita/matita/lib/lambda/cube.ma
+++ b/matita/matita/lib/lambda/cube.ma
@@ -17,27 +17,27 @@ include "types.ma".
 
 (* PURE TYPE SYSTEMS OF THE λ-CUBE ********************************************)
 
-inductive Cube_Ax (i,j:nat): Prop ≝
-  | star_box: i = 0 → j = 1 → Cube_Ax i j
+inductive Cube_Ax: nat → nat → Prop ≝
+  | star_box: Cube_Ax 0 1
 .
 
 (* The λPω pure type system (a.k.a. λC or CC) *********************************)
 
-inductive CC_Re (i,j,k:nat): Prop ≝
-   | star_star: i = 0 → j = 0 → k = 0 → CC_Re i j k
-   | box_star : i = 1 → j = 0 → k = 0 → CC_Re i j k
-   | box_box  : i = 1 → j = 1 → k = 1 → CC_Re i j k
-   | star_box : i = 0 → j = 1 → k = 1 → CC_Re i j k
+inductive CC_Re: nat → nat → nat → Prop ≝
+   | star_star: CC_Re 0 0 0
+   | box_star : CC_Re 1 0 0
+   | box_box  : CC_Re 1 1 1
+   | star_box : CC_Re 0 1 1
 .
 
 definition CC: pts ≝ mk_pts Cube_Ax CC_Re conv.
 
 (* The λω pure type system (a.k.a. Fω) ****************************************)
 
-inductive FO_Re (i,j,k:nat): Prop ≝
-   | star_star: i = 0 → j = 0 → k = 0 → FO_Re i j k
-   | box_star : i = 1 → j = 0 → k = 0 → FO_Re i j k
-   | box_box  : i = 1 → j = 1 → k = 1 → FO_Re i j k
+inductive FO_Re: nat → nat → nat → Prop ≝
+   | star_star: FO_Re 0 0 0
+   | box_star : FO_Re 1 0 0
+   | box_box  : FO_Re 1 1 1
 .
 
 definition FO: pts ≝ mk_pts Cube_Ax FO_Re conv.