update in static_2

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce_drops.ma
index 49bf1e88567369b3f0ddc29ccca205b3bf020fca..6e8afb63c7f156abf0a495e4716680811697f5e0 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce_drops.ma
@@ -22,8 +22,8 @@ include "basic_2/rt_conversion/cpce.ma".
 lemma cpce_eta_drops (h) (n) (G) (K):
       ∀p,W,V1,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V1.U →
       ∀V2. ⦃G,K⦄ ⊢ V1 ⬌η[h] V2 →
-      â\88\80i,L. â¬\87*[i] L ≘ K.ⓛW →
-      â\88\80W2. â¬\86*[↑i] V2 ≘ W2 → ⦃G,L⦄ ⊢ #i ⬌η[h] +ⓛW2.ⓐ#0.#↑i.
+      â\88\80i,L. â\87©*[i] L ≘ K.ⓛW →
+      â\88\80W2. â\87§*[↑i] V2 ≘ W2 → ⦃G,L⦄ ⊢ #i ⬌η[h] +ⓛW2.ⓐ#0.#↑i.
 #h #n #G #K #p #W #V1 #U #HWU #V2 #HV12 #i elim i -i
 [ #L #HLK #W2 #HVW2
   >(drops_fwd_isid … HLK) -L [| // ] /2 width=8 by cpce_eta/
@@ -35,7 +35,7 @@ lemma cpce_eta_drops (h) (n) (G) (K):
 qed.
 
 lemma cpce_zero_drops (h) (G):
-      â\88\80i,L. (â\88\80n,p,K,W,V,U. â¬\87*[i] L ≘ K.ⓛW → ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → ⊥) →
+      â\88\80i,L. (â\88\80n,p,K,W,V,U. â\87©*[i] L ≘ K.ⓛW → ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → ⊥) →
       ⦃G,L⦄ ⊢ #i ⬌η[h] #i.
 #h #G #i elim i -i
 [ * [ #_ // ] #L #I #Hi