|#P #M1 %2 //
]
qed.
-
+(* FG: THIS IN NOT COMPLETE
theorem main1: ∀M,N. CO M N →
∃P,Q. star … red M P ∧ star … red N Q ∧ d_eq P Q.
#M #N #coMN (elim coMN)
[
|@(ex_intro … M) @(ex_intro … M) % // % //
]
-
+*)
lemma red_d : ∀M,P. red (D M) P → ∃N. P = D N ∧ red M N.
#M #P #redMP (inversion redMP)
[#P1 #M1 #N1 #eqH destruct
#M #N #rstar (elim rstar) //
#Q #P #HbQ #redQP #snNQ #snN @(SN_step …redQP) /2/
qed.
-
+(* FG: THIS EXPLODES
lemma sub_red: ∀M,N.subterm N M → ∀N1.red N N1 →
∃M1.subterm N1 M1 ∧ red M M1.
#M #N #subN (elim subN) /4/
#B * #subA #redQ (cases (H2 ? redQ)) #C * #subBC #redSC
@(ex_intro … C) /3/
qed.
-
+*)
axiom sub_star_red: ∀M,N.(star … subterm) N M → ∀N1.red N N1 →
∃M1.subterm N1 M1 ∧ red M M1.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "convertibility.ma".
+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
+.
+
+(* 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
+.
+
+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
+.
+
+definition FO: pts ≝ mk_pts Cube_Ax FO_Re conv.