- 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 9213b4d578d49181ccf8d71c782b7776b20260f3..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