update in static_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_conversion / cpce.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce.ma
index 3da6a15983bd05a8893b04f7f5d01cf76e30128c..7deb96dab6ad2f0573bb27fee012e468486c186f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce.ma
@@ -25,9 +25,9 @@ inductive cpce (h): relation4 genv lenv term term ≝
 | cpce_zero: ∀G,K,I. (∀n,p,W,V,U. I = BPair Abst W → ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → ⊥) →
              cpce h G (K.ⓘ{I}) (#0) (#0)
 | cpce_eta : ∀n,p,G,K,W,V1,V2,W2,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V1.U →
-             cpce h G K V1 V2 â\86\92 â¬\86*[1] V2 ≘ W2 → cpce h G (K.ⓛW) (#0) (+ⓛW2.ⓐ#0.#1)
+             cpce h G K V1 V2 â\86\92 â\87§*[1] V2 ≘ W2 → cpce h G (K.ⓛW) (#0) (+ⓛW2.ⓐ#0.#1)
 | cpce_lref: ∀I,G,K,T,U,i. cpce h G K (#i) T →
-             â¬\86*[1] T ≘ U → cpce h G (K.ⓘ{I}) (#↑i) U
+             â\87§*[1] T ≘ U → cpce h G (K.ⓘ{I}) (#↑i) U
 | cpce_gref: ∀G,L,l. cpce h G L (§l) (§l)
 | cpce_bind: ∀p,I,G,K,V1,V2,T1,T2.
              cpce h G K V1 V2 → cpce h G (K.ⓑ{I}V1) T1 T2 →
@@ -79,7 +79,7 @@ lemma cpce_inv_zero_sn (h) (G) (K) (X2):
       ∀I. ⦃G,K.ⓘ{I}⦄ ⊢ #0 ⬌η[h] X2 →
       ∨∨ ∧∧ ∀n,p,W,V,U. I = BPair Abst W → ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → ⊥ & #0 = X2
        | ∃∃n,p,W,V1,V2,W2,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V1.U & ⦃G,K⦄ ⊢ V1 ⬌η[h] V2
-                           & â¬\86*[1] V2 ≘ W2 & I = BPair Abst W & +ⓛW2.ⓐ#0.#1 = X2.
+                           & â\87§*[1] V2 ≘ W2 & I = BPair Abst W & +ⓛW2.ⓐ#0.#1 = X2.
 #h #G #Y0 #X2 #Z
 @(insert_eq_0 … (Y0.ⓘ{Z})) #Y
 @(insert_eq_0 … (#0)) #X1
@@ -97,7 +97,7 @@ qed-.
 
 lemma cpce_inv_lref_sn (h) (G) (K) (X2):
       ∀I,i. ⦃G,K.ⓘ{I}⦄ ⊢ #↑i ⬌η[h] X2 →
-      â\88\83â\88\83T2. â¦\83G,Kâ¦\84 â\8a¢ #i â¬\8cη[h] T2 & â¬\86*[1] T2 ≘ X2.
+      â\88\83â\88\83T2. â¦\83G,Kâ¦\84 â\8a¢ #i â¬\8cη[h] T2 & â\87§*[1] T2 ≘ X2.
 #h #G #Y0 #X2 #Z #j
 @(insert_eq_0 … (Y0.ⓘ{Z})) #Y
 @(insert_eq_0 … (#↑j)) #X1