X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fcnv_cpm_conf.ma;h=c10e470dd3976498d84cb22e26449c73445d52dc;hb=647b419e96770d90a82d7a9e5e8843566a9f93ee;hp=3e6527a02a3d9db9213b19115e910962aa67b1eb;hpb=4173283e148199871d787c53c0301891deb90713;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_conf.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_conf.ma
index 3e6527a02..c10e470dd 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_conf.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_conf.ma
@@ -24,11 +24,11 @@ include "basic_2/dynamic/cnv_preserve_sub.ma".
 (* Sub diamond propery with t-bound rt-transition for terms *****************)
 
 fact cnv_cpm_conf_lpr_atom_atom_aux (h) (G) (L1) (L2) (I):
-     ∃∃T. ⦃G,L1⦄ ⊢ ⓪{I} ➡*[0,h] T & ⦃G, L2⦄ ⊢ ⓪{I} ➡*[O,h] T.
+     ∃∃T. ⦃G,L1⦄ ⊢ ⓪{I} ➡*[0,h] T & ⦃G,L2⦄ ⊢ ⓪{I} ➡*[O,h] T.
 /2 width=3 by ex2_intro/ qed-.
 
 fact cnv_cpm_conf_lpr_atom_ess_aux (h) (G) (L1) (L2) (s):
-     ∃∃T. ⦃G,L1⦄ ⊢ ⋆s ➡*[1,h] T & ⦃G,L2⦄ ⊢ ⋆(next h s) ➡*[h] T.
+     ∃∃T. ⦃G,L1⦄ ⊢ ⋆s ➡*[1,h] T & ⦃G,L2⦄ ⊢ ⋆(⫯[h]s) ➡*[h] T.
 /3 width=3 by cpm_cpms, ex2_intro/ qed-.
 
 fact cnv_cpm_conf_lpr_atom_delta_aux (a) (h) (G) (L) (i):
@@ -40,7 +40,7 @@ fact cnv_cpm_conf_lpr_atom_delta_aux (a) (h) (G) (L) (i):
      ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
      ∃∃T. ⦃G,L1⦄ ⊢ #i ➡*[n,h] T & ⦃G,L2⦄ ⊢ X ➡*[h] T.
 #a #h #G #L #i #IH #HT #K #V #HLK #n #XV #HVX #X #HXV #L1 #HL1 #L2 #HL2
-lapply (cnv_lref_fwd_drops … HT … HLK) -HT #HV
+lapply (cnv_inv_lref_pair … HT … HLK) -HT #HV
 elim (lpr_drops_conf … HLK … HL1) -HL1 // #Y1 #H1 #HLK1
 elim (lpr_inv_pair_sn … H1) -H1 #K1 #V1 #HK1 #HV1 #H destruct
 elim (lpr_drops_conf … HLK … HL2) -HL2 // #Y2 #H2 #HLK2
@@ -62,7 +62,7 @@ fact cnv_cpm_conf_lpr_atom_ell_aux (a) (h) (G) (L) (i):
      ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
      ∃∃T. ⦃G,L1⦄ ⊢ #i ➡*[↑n,h] T & ⦃G,L2⦄ ⊢ X ➡*[h] T.
 #a #h #G #L #i #IH #HT #K #W #HLK #n #XW #HWX #X #HXW #L1 #HL1 #L2 #HL2
-lapply (cnv_lref_fwd_drops … HT … HLK) -HT #HW
+lapply (cnv_inv_lref_pair … HT … HLK) -HT #HW
 elim (lpr_drops_conf … HLK … HL1) -HL1 // #Y1 #H1 #HLK1
 elim (lpr_inv_pair_sn … H1) -H1 #K1 #W1 #HK1 #HW1 #H destruct
 elim (lpr_drops_conf … HLK … HL2) -HL2 // #Y2 #H2 #HLK2
@@ -87,7 +87,7 @@ fact cnv_cpm_conf_lpr_delta_delta_aux (a) (h) (I) (G) (L) (i):
 #K #V #HLK #Y #X #HLY #n1 #XV1 #HVX1 #n2 #XV2 #HVX2 #X1 #HXV1 #X2 #HXV2
 #L1 #HL1 #L2 #HL2
 lapply (drops_mono … HLY … HLK) -HLY #H destruct
-lapply (cnv_lref_fwd_drops … HT … HLK) -HT #HV
+lapply (cnv_inv_lref_pair … HT … HLK) -HT #HV
 elim (lpr_drops_conf … HLK … HL1) -HL1 // #Y1 #H1 #HLK1
 elim (lpr_inv_pair_sn … H1) -H1 #K1 #V1 #HK1 #_ #H destruct
 lapply (drops_isuni_fwd_drop2 … HLK1) -V1 // #HLK1
@@ -388,8 +388,8 @@ qed-.
 
 fact cnv_cpm_conf_lpr_aux (a) (h):
                           ∀G0,L0,T0.
-                          (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h] ⦃G1, L1, T1⦄ → IH_cnv_cpm_trans_lpr a h G1 L1 T1) →
-                          (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h] ⦃G1, L1, T1⦄ → IH_cnv_cpms_conf_lpr a h G1 L1 T1) →
+                          (∀G1,L1,T1. ⦃G0,L0,T0⦄ >[h] ⦃G1,L1,T1⦄ → IH_cnv_cpm_trans_lpr a h G1 L1 T1) →
+                          (∀G1,L1,T1. ⦃G0,L0,T0⦄ >[h] ⦃G1,L1,T1⦄ → IH_cnv_cpms_conf_lpr a h G1 L1 T1) →
                           ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_cnv_cpm_conf_lpr a h G1 L1 T1.
 #a #h #G0 #L0 #T0 #IH2 #IH1 #G #L * [| * [| * ]]
 [ #I #HG0 #HL0 #HT0 #HT #n1 #X1 #HX1 #n2 #X2 #HX2 #L1 #HL1 #L2 #HL2 destruct