update in static_2

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_cpms.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_cpms.ma
index 591dbd1c1eeb46bbfa180b0e09ab75f14aae0af6..c75c79f8f58085c295a11dfde865510940d0ef5a 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_cpms.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_cpms.ma
@@ -75,7 +75,7 @@ qed-.
 lemma cpms_inv_abbr_sn_dx (n) (h) (G) (L):
                           ∀p,V1,T1,X2. ⦃G,L⦄ ⊢ ⓓ{p}V1.T1 ➡*[n,h] X2 →
                           ∨∨ ∃∃V2,T2. ⦃G,L⦄ ⊢ V1 ➡*[h] V2 & ⦃G,L.ⓓV1⦄ ⊢ T1 ➡*[n,h] T2 & X2 = ⓓ{p}V2.T2
-                           | â\88\83â\88\83T2. â¦\83G,L.â\93\93V1â¦\84 â\8a¢ T1 â\9e¡*[n ,h] T2 & â¬\86*[1] X2 ≘ T2 & p = Ⓣ.
+                           | â\88\83â\88\83T2. â¦\83G,L.â\93\93V1â¦\84 â\8a¢ T1 â\9e¡*[n ,h] T2 & â\87§*[1] X2 ≘ T2 & p = Ⓣ.
 #n #h #G #L #p #V1 #T1 #X2 #H
 @(cpms_ind_dx … H) -X2 -n /3 width=5 by ex3_2_intro, or_introl/
 #n1 #n2 #X #X2 #_ * *
@@ -96,7 +96,7 @@ qed-.
 (* Basic_2A1: uses: scpds_inv_abbr_abst *)
 lemma cpms_inv_abbr_abst (n) (h) (G) (L):
                          ∀p1,p2,V1,W2,T1,T2. ⦃G,L⦄ ⊢ ⓓ{p1}V1.T1 ➡*[n,h] ⓛ{p2}W2.T2 →
-                         â\88\83â\88\83T. â¦\83G,L.â\93\93V1â¦\84 â\8a¢ T1 â\9e¡*[n,h] T & â¬\86*[1] ⓛ{p2}W2.T2 ≘ T & p1 = Ⓣ.
+                         â\88\83â\88\83T. â¦\83G,L.â\93\93V1â¦\84 â\8a¢ T1 â\9e¡*[n,h] T & â\87§*[1] ⓛ{p2}W2.T2 ≘ T & p1 = Ⓣ.
 #n #h #G #L #p1 #p2 #V1 #W2 #T1 #T2 #H
 elim (cpms_inv_abbr_sn_dx … H) -H *
 [ #V #T #_ #_ #H destruct