notational change of lift, drop, and gget

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / dynamic / snv_lift.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma
index 0d604c128bbf6159dda85ae1569ced527068bf28..09acef6c3d28da24522ded2162238f095a57f33e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma
@@ -20,8 +20,8 @@ include "basic_2/dynamic/snv.ma".
 
 (* Relocation properties ****************************************************)
 
-lemma snv_lift: â\88\80h,g,G,K,T. â¦\83G, Kâ¦\84 â\8a¢ T ¡[h, g] â\86\92 â\88\80L,s,d,e. â\87©[s, d, e] L ≡ K →
-                â\88\80U. â\87§[d, e] T ≡ U → ⦃G, L⦄ ⊢ U ¡[h, g].
+lemma snv_lift: â\88\80h,g,G,K,T. â¦\83G, Kâ¦\84 â\8a¢ T ¡[h, g] â\86\92 â\88\80L,s,d,e. â¬\87[s, d, e] L ≡ K →
+                â\88\80U. â¬\86[d, e] T ≡ U → ⦃G, L⦄ ⊢ U ¡[h, g].
 #h #g #G #K #T #H elim H -G -K -T
 [ #G #K #k #L #s #d #e #_ #X #H
   >(lift_inv_sort1 … H) -X -K -d -e //
@@ -49,8 +49,8 @@ lemma snv_lift: ∀h,g,G,K,T. ⦃G, K⦄ ⊢ T ¡[h, g] → ∀L,s,d,e. ⇩[s, d
 ]
 qed.
 
-lemma snv_inv_lift: â\88\80h,g,G,L,U. â¦\83G, Lâ¦\84 â\8a¢ U ¡[h, g] â\86\92 â\88\80K,s,d,e. â\87©[s, d, e] L ≡ K →
-                    â\88\80T. â\87§[d, e] T ≡ U → ⦃G, K⦄ ⊢ T ¡[h, g].
+lemma snv_inv_lift: â\88\80h,g,G,L,U. â¦\83G, Lâ¦\84 â\8a¢ U ¡[h, g] â\86\92 â\88\80K,s,d,e. â¬\87[s, d, e] L ≡ K →
+                    â\88\80T. â¬\86[d, e] T ≡ U → ⦃G, K⦄ ⊢ T ¡[h, g].
 #h #g #G #L #U #H elim H -G -L -U
 [ #G #L #k #K #s #d #e #_ #X #H
   >(lift_inv_sort2 … H) -X -L -d -e //