notational change of lift, drop, and gget

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / reduction / crr_lift.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/crr_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/crr_lift.ma
index 27a6951bdf9874413559c6e877e2211c870ccbd0..ee142ffe3c152d398ad527efa23eaea947e748e9 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/crr_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/crr_lift.ma
@@ -19,8 +19,8 @@ include "basic_2/reduction/crr.ma".
 
 (* Properties on relocation *************************************************)
 
-lemma crr_lift: â\88\80G,K,T. â¦\83G, Kâ¦\84 â\8a¢ â\9e¡ ð\9d\90\91â¦\83Tâ¦\84 â\86\92 â\88\80L,s,d,e. â\87©[s, d, e] L ≡ K →
-                â\88\80U. â\87§[d, e] T ≡ U → ⦃G, L⦄ ⊢ ➡ 𝐑⦃U⦄.
+lemma crr_lift: â\88\80G,K,T. â¦\83G, Kâ¦\84 â\8a¢ â\9e¡ ð\9d\90\91â¦\83Tâ¦\84 â\86\92 â\88\80L,s,d,e. â¬\87[s, d, e] L ≡ K →
+                â\88\80U. â¬\86[d, e] T ≡ U → ⦃G, L⦄ ⊢ ➡ 𝐑⦃U⦄.
 #G #K #T #H elim H -K -T
 [ #K #K0 #V #i #HK0 #L #s #d #e #HLK #X #H
   elim (lift_inv_lref1 … H) -H * #Hid #H destruct
@@ -46,8 +46,8 @@ lemma crr_lift: ∀G,K,T. ⦃G, K⦄ ⊢ ➡ 𝐑⦃T⦄ → ∀L,s,d,e. ⇩[s,
 ]
 qed.
 
-lemma crr_inv_lift: â\88\80G,L,U. â¦\83G, Lâ¦\84 â\8a¢ â\9e¡ ð\9d\90\91â¦\83Uâ¦\84 â\86\92 â\88\80K,s,d,e. â\87©[s, d, e] L ≡ K →
-                    â\88\80T. â\87§[d, e] T ≡ U → ⦃G, K⦄ ⊢ ➡ 𝐑⦃T⦄.
+lemma crr_inv_lift: â\88\80G,L,U. â¦\83G, Lâ¦\84 â\8a¢ â\9e¡ ð\9d\90\91â¦\83Uâ¦\84 â\86\92 â\88\80K,s,d,e. â¬\87[s, d, e] L ≡ K →
+                    â\88\80T. â¬\86[d, e] T ≡ U → ⦃G, K⦄ ⊢ ➡ 𝐑⦃T⦄.
 #G #L #U #H elim H -L -U
 [ #L #L0 #W #i #HK0 #K #s #d #e #HLK #X #H
   elim (lift_inv_lref2 … H) -H * #Hid #H destruct