X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fcnv_etc.ma;h=d7ac516cd55f929e0499027e36fc4f4326a80c9e;hp=c2e0809f814bc37915cca882e0b60d455a22b48c;hb=93768d9ebc0e3c8e3bcd69571d7a635cb1a16b29;hpb=b634a816745cf8a9a7ad14650d088232c8ee1a1a

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_etc.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_etc.ma
index c2e0809f8..d7ac516cd 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_etc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_etc.ma
@@ -48,16 +48,23 @@ definition IH_cnv_cpms_conf_lpr (a) (h): relation3 genv lenv term ≝
                                 ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 →
                                 ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G, L2⦄ ⊢ T2 ➡*[n1-n2,h] T.
 
-(* Auxiliary properties for preservation ************************************)
+(* Properties for preservation **********************************************)
 
-fact cnv_cpms_trans_lpr_aux (a) (h) (o):
-                            ∀G0,L0,T0.
-                            (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_trans_lpr a h G1 L1 T1) →
-                            ∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_trans_lpr a h G1 L1 T1.
+lemma cnv_cpms_trans_lpr_far (a) (h) (o):
+                             ∀G0,L0,T0.
+                             (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_trans_lpr a h G1 L1 T1) →
+                             ∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_trans_lpr a h G1 L1 T1.
 #a #h #o #G0 #L0 #T0 #IH #G1 #L1 #T1 #H01 #HT1 #n #T2 #H
 @(cpms_ind_dx … H) -n -T2
 /4 width=7 by cpms_fwd_fpbs, fpbg_fpbs_trans/
 qed-.
+
+lemma cnv_cpms_strip_lpr_far (a) (h) (o):
+                             ∀G0,L0,T0.
+                             (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_conf_lpr a h G1 L1 T1) →
+                             ∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_strip_lpr a h G1 L1 T1.
+/3 width=8 by cpm_cpms/ qed-.
+
 (*
 fact cnv_cpms_strip_lpr_aux (a) (h) (o):
                             ∀G0,L0,T0.