first definition of cpm:

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_transition / cpx.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma
index c7dde663e8dfa0e6fc0ea7d379f44a6461995da9..9900e8bf1cd088fcafad53a2a3633475df8fdc3d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma
@@ -26,9 +26,6 @@ interpretation
 
 (* Basic properties *********************************************************)
 
-lemma cpx_atom: ∀h,I,G,L. ⦃G, L⦄ ⊢ ⓪{I} ⬈[h] ⓪{I}.
-/2 width=2 by cpg_atom, ex_intro/ qed.
-
 (* Basic_2A1: was: cpx_st *)
 lemma cpx_ess: ∀h,G,L,s. ⦃G, L⦄ ⊢ ⋆s ⬈[h] ⋆(next h s).
 /2 width=2 by cpg_ess, ex_intro/ qed.
@@ -46,15 +43,15 @@ lemma cpx_lref: ∀h,I,G,K,V,T,U,i. ⦃G, K⦄ ⊢ #i ⬈[h] T →
 qed.
 
 lemma cpx_bind: ∀h,p,I,G,L,V1,V2,T1,T2.
-                 ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ⬈[h] T2 →
-                 ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈[h] ⓑ{p,I}V2.T2.
+                ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ⬈[h] T2 →
+                ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈[h] ⓑ{p,I}V2.T2.
 #h #p #I #G #L #V1 #V2 #T1 #T2 * #cV #HV12 *
 /3 width=2 by cpg_bind, ex_intro/
 qed.
 
 lemma cpx_flat: ∀h,I,G,L,V1,V2,T1,T2.
-                 ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → ⦃G, L⦄ ⊢ T1 ⬈[h] T2 →
-                 ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ⬈[h] ⓕ{I}V2.T2.
+                ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → ⦃G, L⦄ ⊢ T1 ⬈[h] T2 →
+                ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ⬈[h] ⓕ{I}V2.T2.
 #h #I #G #L #V1 #V2 #T1 #T2 * #cV #HV12 *
 /3 width=2 by cpg_flat, ex_intro/
 qed.
@@ -91,6 +88,7 @@ lemma cpx_theta: ∀h,p,G,L,V1,V,V2,W1,W2,T1,T2.
 /3 width=4 by cpg_theta, ex_intro/
 qed.
 
+(* Basic_2A1: includes: cpx_atom *)
 lemma cpx_refl: ∀h,G,L. reflexive … (cpx h G L).
 /2 width=2 by ex_intro/ qed.