update in static_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / cpxs_toeq_vector.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_toeq_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_toeq_vector.ma
index bbd7c5c9def31a611380d507993b9214a5f8bcb4..20702a3546b1c91bc2980ad8ea02bf19ad415d8d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_toeq_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_toeq_vector.ma
@@ -37,8 +37,8 @@ qed-.
 
 (* Basic_2A1: was: cpxs_fwd_delta_vector *)
 lemma cpxs_fwd_delta_drops_vector (h) (I) (G) (L) (K):
-      â\88\80V1,i. â¬\87*[i] L ≘ K.ⓑ{I}V1 →
-      â\88\80V2. â¬\86*[↑i] V1 ≘ V2 →
+      â\88\80V1,i. â\87©*[i] L ≘ K.ⓑ{I}V1 →
+      â\88\80V2. â\87§*[↑i] V1 ≘ V2 →
       ∀Vs,X2. ⦃G,L⦄ ⊢ ⒶVs.#i ⬈*[h] X2 →
       ∨∨ ⒶVs.#i ⩳ X2 | ⦃G,L⦄ ⊢ ⒶVs.V2 ⬈*[h] X2.
 #h #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs
@@ -90,7 +90,7 @@ qed-.
 
 (* Basic_1: was just: pr3_iso_appls_abbr *)
 lemma cpxs_fwd_theta_vector (h) (G) (L):
-      â\88\80V1b,V2b. â¬\86*[1] V1b ≘ V2b →
+      â\88\80V1b,V2b. â\87§*[1] V1b ≘ V2b →
       ∀p,V,T,X2. ⦃G,L⦄ ⊢ ⒶV1b.ⓓ{p}V.T ⬈*[h] X2 →
       ∨∨ ⒶV1b.ⓓ{p}V.T ⩳ X2 | ⦃G,L⦄ ⊢ ⓓ{p}V.ⒶV2b.T ⬈*[h] X2.
 #h #G #L #V1b #V2b * -V1b -V2b /3 width=1 by or_intror/