update in static_2

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_drops.ma
index 09ba0f251932c474629c31958aaeed997f4a49a4..92c0ca4b611b72d97f7ee3ee6d05d41280e128e9 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_drops.ma
@@ -21,7 +21,7 @@ include "basic_2/rt_computation/cpxs.ma".
 (* Advanced properties ******************************************************)
 
 lemma cpxs_delta: ∀h,I,G,K,V1,V2. ⦃G,K⦄ ⊢ V1 ⬈*[h] V2 →
-                  â\88\80W2. â¬\86*[1] V2 ≘ W2 → ⦃G,K.ⓑ{I}V1⦄ ⊢ #0 ⬈*[h] W2.
+                  â\88\80W2. â\87§*[1] V2 ≘ W2 → ⦃G,K.ⓑ{I}V1⦄ ⊢ #0 ⬈*[h] W2.
 #h #I #G #K #V1 #V2 #H @(cpxs_ind … H) -V2
 [ /3 width=3 by cpx_cpxs, cpx_delta/
 | #V #V2 #_ #HV2 #IH #W2 #HVW2
@@ -31,7 +31,7 @@ lemma cpxs_delta: ∀h,I,G,K,V1,V2. ⦃G,K⦄ ⊢ V1 ⬈*[h] V2 →
 qed.
 
 lemma cpxs_lref: ∀h,I,G,K,T,i. ⦃G,K⦄ ⊢ #i ⬈*[h] T →
-                 â\88\80U. â¬\86*[1] T ≘ U → ⦃G,K.ⓘ{I}⦄ ⊢ #↑i ⬈*[h] U.
+                 â\88\80U. â\87§*[1] T ≘ U → ⦃G,K.ⓘ{I}⦄ ⊢ #↑i ⬈*[h] U.
 #h #I #G #K #T #i #H @(cpxs_ind … H) -T
 [ /3 width=3 by cpx_cpxs, cpx_lref/
 | #T0 #T #_ #HT2 #IH #U #HTU
@@ -42,8 +42,8 @@ qed.
 
 (* Basic_2A1: was: cpxs_delta *)
 lemma cpxs_delta_drops: ∀h,I,G,L,K,V1,V2,i.
-                        â¬\87*[i] L ≘ K.ⓑ{I}V1 → ⦃G,K⦄ ⊢ V1 ⬈*[h] V2 →
-                        â\88\80W2. â¬\86*[↑i] V2 ≘ W2 → ⦃G,L⦄ ⊢ #i ⬈*[h] W2.
+                        â\87©*[i] L ≘ K.ⓑ{I}V1 → ⦃G,K⦄ ⊢ V1 ⬈*[h] V2 →
+                        â\88\80W2. â\87§*[↑i] V2 ≘ W2 → ⦃G,L⦄ ⊢ #i ⬈*[h] W2.
 #h #I #G #L #K #V1 #V2 #i #HLK #H @(cpxs_ind … H) -V2
 [ /3 width=7 by cpx_cpxs, cpx_delta_drops/
 | #V #V2 #_ #HV2 #IH #W2 #HVW2
@@ -56,7 +56,7 @@ qed.
 
 lemma cpxs_inv_zero1: ∀h,G,L,T2. ⦃G,L⦄ ⊢ #0 ⬈*[h] T2 →
                       T2 = #0 ∨
-                      â\88\83â\88\83I,K,V1,V2. â¦\83G,Kâ¦\84 â\8a¢ V1 â¬\88*[h] V2 & â¬\86*[1] V2 ≘ T2 &
+                      â\88\83â\88\83I,K,V1,V2. â¦\83G,Kâ¦\84 â\8a¢ V1 â¬\88*[h] V2 & â\87§*[1] V2 ≘ T2 &
                                    L = K.ⓑ{I}V1.
 #h #G #L #T2 #H @(cpxs_ind … H) -T2 /2 width=1 by or_introl/
 #T #T2 #_ #HT2 *
@@ -71,7 +71,7 @@ qed-.
 
 lemma cpxs_inv_lref1: ∀h,G,L,T2,i. ⦃G,L⦄ ⊢ #↑i ⬈*[h] T2 →
                       T2 = #(↑i) ∨
-                      â\88\83â\88\83I,K,T. â¦\83G,Kâ¦\84 â\8a¢ #i â¬\88*[h] T & â¬\86*[1] T ≘ T2 & L = K.ⓘ{I}.
+                      â\88\83â\88\83I,K,T. â¦\83G,Kâ¦\84 â\8a¢ #i â¬\88*[h] T & â\87§*[1] T ≘ T2 & L = K.ⓘ{I}.
 #h #G #L #T2 #i #H @(cpxs_ind … H) -T2 /2 width=1 by or_introl/
 #T #T2 #_ #HT2 *
 [ #H destruct
@@ -86,8 +86,8 @@ qed-.
 (* Basic_2A1: was: cpxs_inv_lref1 *)
 lemma cpxs_inv_lref1_drops: ∀h,G,L,T2,i. ⦃G,L⦄ ⊢ #i ⬈*[h] T2 →
                             T2 = #i ∨
-                            â\88\83â\88\83I,K,V1,T1. â¬\87*[i] L ≘ K.ⓑ{I}V1 & ⦃G,K⦄ ⊢ V1 ⬈*[h] T1 &
-                                         â¬\86*[↑i] T1 ≘ T2.
+                            â\88\83â\88\83I,K,V1,T1. â\87©*[i] L ≘ K.ⓑ{I}V1 & ⦃G,K⦄ ⊢ V1 ⬈*[h] T1 &
+                                         â\87§*[↑i] T1 ≘ T2.
 #h #G #L #T2 #i #H @(cpxs_ind … H) -T2 /2 width=1 by or_introl/
 #T #T2 #_ #HT2 *
 [ #H destruct