update in static_2

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms.ma
index 2f7d1f449b826168cc3ec6c31f53048f22657732..081eece9b1257698327268c01aa216e38beeafc5 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms.ma
@@ -80,7 +80,7 @@ lemma cpms_appl_dx (n) (h) (G) (L):
 qed.
 
 lemma cpms_zeta (n) (h) (G) (L):
-                â\88\80T1,T. â¬\86*[1] T ≘ T1 →
+                â\88\80T1,T. â\87§*[1] T ≘ T1 →
                 ∀V,T2. ⦃G,L⦄ ⊢ T ➡*[n,h] T2 → ⦃G,L⦄ ⊢ +ⓓV.T1 ➡*[n,h] T2.
 #n #h #G #L #T1 #T #HT1 #V #T2 #H @(cpms_ind_dx … H) -T2
 /3 width=3 by cpms_step_dx, cpm_cpms, cpm_zeta/
@@ -88,7 +88,7 @@ qed.
 
 (* Basic_2A1: uses: cprs_zeta *)
 lemma cpms_zeta_dx (n) (h) (G) (L):
-                   â\88\80T2,T. â¬\86*[1] T2 ≘ T →
+                   â\88\80T2,T. â\87§*[1] T2 ≘ T →
                    ∀V,T1. ⦃G,L.ⓓV⦄ ⊢ T1 ➡*[n,h] T → ⦃G,L⦄ ⊢ +ⓓV.T1 ➡*[n,h] T2.
 #n #h #G #L #T2 #T #HT2 #V #T1 #H @(cpms_ind_sn … H) -T1
 /3 width=3 by cpms_step_sn, cpm_cpms, cpm_bind, cpm_zeta/
@@ -125,7 +125,7 @@ qed.
 (* Basic_2A1: uses: cprs_theta_dx *)
 lemma cpms_theta_dx (n) (h) (G) (L):
                     ∀V1,V. ⦃G,L⦄ ⊢ V1 ➡[h] V →
-                    â\88\80V2. â¬\86*[1] V ≘ V2 →
+                    â\88\80V2. â\87§*[1] V ≘ V2 →
                     ∀W1,W2. ⦃G,L⦄ ⊢ W1 ➡[h] W2 →
                     ∀T1,T2. ⦃G,L.ⓓW1⦄ ⊢ T1 ➡*[n,h] T2 →
                     ∀p. ⦃G,L⦄ ⊢ ⓐV1.ⓓ{p}W1.T1 ➡*[n,h] ⓓ{p}W2.ⓐV2.T2.
@@ -144,7 +144,7 @@ lemma cprs_refl: ∀h,G,L. reflexive … (cpms h G L 0).
 lemma cpms_sort (h) (G) (L) (n):
                 ∀s. ⦃G,L⦄ ⊢ ⋆s ➡*[n,h] ⋆((next h)^n s).
 #h #G #L #n elim n -n [ // ]
-#n #IH #s <plus_SO
+#n #IH #s <plus_SO_dx
 /3 width=3 by cpms_step_dx, cpm_sort/
 qed.