- advances in the theory of cofrees

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma
index a7b6e3e7787d4fb024865b02641bd3734ebd6946..1ee5ba08ec4cf80bfefd4f3e092a91f8d8b63484 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma
@@ -22,10 +22,10 @@ include "basic_2/dynamic/lsubsv_lsstas.ma".
 (* Properties on sn parallel reduction for local environments ***************)
 
 fact lsstas_cpr_lpr_aux: ∀h,g,G0,L0,T0.
-                         (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\8b\95[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) →
-                         (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\8b\95[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
-                         (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\8b\95[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
-                         (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\8b\95[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) →
+                         (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) →
+                         (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+                         (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) →
+                         (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) →
                          ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_lsstas_cpr_lpr h g G1 L1 T1.
 #h #g #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| * ]
 [ #k #_ #_ #_ #_ #l1 #l2 #_ #_ #X2 #H2 #X3 #H3 #L2 #_ -IH4 -IH3 -IH2 -IH1
@@ -52,13 +52,13 @@ fact lsstas_cpr_lpr_aux: ∀h,g,G0,L0,T0.
   ]
   [ elim (IH1 … HWl1 … HW0 … HW12 … HK12) -IH1 -HW0 /2 width=1 by fqup_fpbg/ #V2 #HWV2 #HV2
     elim (lift_total V2 0 (i+1))
-    /6 width=11 by fqup_fpbg, cpcs_lift, lsstas_ldec, ex2_intro/
+    /6 width=12 by fqup_fpbg, cpcs_lift, lsstas_ldec, ex2_intro/
   | elim (IH1 … HVl1 … HW0 … HV12 … HK12) -IH1 -HVl1 -HW0 -HV12 -HK12 -IH2 /2 width=1 by fqup_fpbg/ #W2 #HVW2 #HW02
     elim (lift_total W2 0 (i+1))
-    /4 width=11 by cpcs_lift, lsstas_ldef, ex2_intro/
+    /4 width=12 by cpcs_lift, lsstas_ldef, ex2_intro/
   | elim (IH1 … HVl1 … HW0 … HVX0 … HK12) -IH1 -HVl1 -HW0 -HVX0 -HK12 -IH2 -V2 /2 width=1 by fqup_fpbg/ -l1 #W2 #HXW2 #HW02
     elim (lift_total W2 0 (i+1))
-    /3 width=11 by cpcs_lift, lsstas_lift, ex2_intro/
+    /3 width=12 by cpcs_lift, lsstas_lift, ex2_intro/
   ]
 | #p #_ #_ #HT0 #H1 destruct -IH4 -IH3 -IH2 -IH1
   elim (snv_inv_gref … H1)