notational change of lift, drop, and gget

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / cpxs_tsts.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tsts.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tsts.ma
index b1d0f1116c03632027ea7a024cceed64f69a9fd5..2991481d92a4033a8a965a49c3f897a73c190212 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tsts.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tsts.ma
@@ -56,8 +56,8 @@ elim (cpxs_inv_appl1 … H) -H *
 qed-.
 
 (* Note: probably this is an inversion lemma *)
-lemma cpxs_fwd_delta: â\88\80h,g,I,G,L,K,V1,i. â\87©[i] L ≡ K.ⓑ{I}V1 →
-                      â\88\80V2. â\87§[0, i + 1] V1 ≡ V2 →
+lemma cpxs_fwd_delta: â\88\80h,g,I,G,L,K,V1,i. â¬\87[i] L ≡ K.ⓑ{I}V1 →
+                      â\88\80V2. â¬\86[0, i + 1] V1 ≡ V2 →
                       ∀U. ⦃G, L⦄ ⊢ #i ➡*[h, g] U →
                       #i ≂ U ∨ ⦃G, L⦄ ⊢ V2 ➡*[h, g] U.
 #h #g #I #G #L #K #V1 #i #HLK #V2 #HV12 #U #H
@@ -68,7 +68,7 @@ lapply (drop_mono … HLK0 … HLK) -HLK0 #H destruct
 qed-.
 
 lemma cpxs_fwd_theta: ∀h,g,a,G,L,V1,V,T,U. ⦃G, L⦄ ⊢ ⓐV1.ⓓ{a}V.T ➡*[h, g] U →
-                      â\88\80V2. â\87§[0, 1] V1 ≡ V2 → ⓐV1.ⓓ{a}V.T ≂ U ∨
+                      â\88\80V2. â¬\86[0, 1] V1 ≡ V2 → ⓐV1.ⓓ{a}V.T ≂ U ∨
                       ⦃G, L⦄ ⊢ ⓓ{a}V.ⓐV2.T ➡*[h, g] U.
 #h #g #a #G #L #V1 #V #T #U #H #V2 #HV12
 elim (cpxs_inv_appl1 … H) -H *