X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fcnv_preserve_sub.ma;h=ce9c46f7e43ca3b721c76de74dff48d559e5b60d;hp=c99d6a5c08a7387f6416eee775775f3b520f73fd;hb=4173283e148199871d787c53c0301891deb90713;hpb=a67fc50ccfda64377e2c94c18c3a0d9265f651db

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_sub.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_sub.ma
index c99d6a5c0..ce9c46f7e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_sub.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_sub.ma
@@ -49,23 +49,23 @@ definition IH_cnv_cpms_conf_lpr (a) (h): relation3 genv lenv term ≝
 
 (* Auxiliary properties for preservation ************************************)
 
-fact cnv_cpms_trans_lpr_sub (a) (h) (o):
+fact cnv_cpms_trans_lpr_sub (a) (h):
                             ∀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
+                            (∀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_trans_lpr a h G1 L1 T1.
+#a #h #G0 #L0 #T0 #IH #G1 #L1 #T1 #H01 #HT1 #n #T2 #H
 @(cpms_ind_dx … H) -n -T2
 /3 width=7 by fpbg_cpms_trans/
 qed-.
 
-fact cnv_cpm_conf_lpr_sub (a) (h) (o):
+fact cnv_cpm_conf_lpr_sub (a) (h):
                           ∀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_cpm_conf_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_conf_lpr a h G1 L1 T1.
 /3 width=8 by cpm_cpms/ qed-.
 
-fact cnv_cpms_strip_lpr_sub (a) (h) (o):
+fact cnv_cpms_strip_lpr_sub (a) (h):
                             ∀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.
+                            (∀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_cpms_strip_lpr a h G1 L1 T1.
 /3 width=8 by cpm_cpms/ qed-.