still more additions and corrections for the article

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

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 2eedc2889194bbf636c00ec0e1b49d8f0aedb092..244f82718e30cfc48a5d355a44ae6a28efc31124 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_sub.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_sub.ma
@@ -50,22 +50,22 @@ definition IH_cnv_cpms_conf_lpr (a) (h): relation3 genv lenv term ≝
 (* Auxiliary properties for preservation ************************************)
 
 fact cnv_cpms_trans_lpr_sub (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_trans_lpr a h G1 L1 T1.
+     ∀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_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):
-                          ∀G0,L0,T0.
-                          (∀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.
+     ∀G0,L0,T0.
+     (∀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):
-                            ∀G0,L0,T0.
-                            (∀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.
+     ∀G0,L0,T0.
+     (∀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-.