milestone in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / dynamic / cnv_cpm_tdeq.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq.ma
index c02e3007773dc7c7d4ff36ff85d7ed54e149c3d2..d1f41252b324613c6b4132405056b20914957d76 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq.ma
@@ -15,7 +15,6 @@
 include "ground_2/xoa/ex_5_1.ma".
 include "ground_2/xoa/ex_9_3.ma".
 include "basic_2/rt_transition/cpm_tdeq.ma".
-include "basic_2/rt_transition/cpr.ma".
 include "basic_2/rt_computation/fpbg_fqup.ma".
 include "basic_2/dynamic/cnv_fsb.ma".
 
@@ -76,7 +75,7 @@ qed-.
 lemma cpm_tdeq_inv_appl_sn (a) (h) (n) (G) (L):
                            ∀V,T1. ⦃G,L⦄ ⊢ ⓐV.T1 ![a,h] →
                            ∀X. ⦃G,L⦄ ⊢ ⓐV.T1 ➡[n,h] X → ⓐV.T1 ≛ X →
-                           ∃∃m,q,W,U1,T2. a = Ⓣ → m ≤ 1 & ⦃G,L⦄ ⊢ V ![a,h] & ⦃G, L⦄ ⊢ V ➡*[1,h] W & ⦃G, L⦄ ⊢ T1 ➡*[m,h] ⓛ{q}W.U1
+                           ∃∃m,q,W,U1,T2. yinj m < a & ⦃G,L⦄ ⊢ V ![a,h] & ⦃G, L⦄ ⊢ V ➡*[1,h] W & ⦃G, L⦄ ⊢ T1 ➡*[m,h] ⓛ{q}W.U1
                                         & ⦃G,L⦄⊢ T1 ![a,h] & ⦃G, L⦄ ⊢ T1 ➡[n,h] T2 & T1 ≛ T2 & X = ⓐV.T2.
 #a #h #n #G #L #V #T1 #H0 #X #H1 #H2
 elim (cpm_inv_appl1 … H1) -H1 *
@@ -134,7 +133,7 @@ lemma cpm_tdeq_ind (a) (h) (n) (G) (Q:relation3 …):
                     ∀T2. ⦃G,L.ⓑ{I}V⦄ ⊢ T1 ➡[n,h] T2 → T1 ≛ T2 →
                     Q (L.ⓑ{I}V) T1 T2 → Q L (ⓑ{p,I}V.T1) (ⓑ{p,I}V.T2)
                    ) →
-                   (∀m. (a = Ⓣ → m ≤ 1) →
+                   (∀m. yinj m < a →
                     ∀L,V. ⦃G,L⦄ ⊢ V ![a,h] → ∀W. ⦃G, L⦄ ⊢ V ➡*[1,h] W →
                     ∀p,T1,U1. ⦃G, L⦄ ⊢ T1 ➡*[m,h] ⓛ{p}W.U1 → ⦃G,L⦄⊢ T1 ![a,h] →
                     ∀T2. ⦃G, L⦄ ⊢ T1 ➡[n,h] T2 → T1 ≛ T2 →