notational change of lift, drop, and gget

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_lift.ma
index b570745d90245e7032a1f5757f63452a162c4b1b..b9f4102a6c0da0188cbe9fcca0496893f7eaf233 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_lift.ma
@@ -19,10 +19,10 @@ include "basic_2/reduction/cir.ma".
 
 (* Properties on relocation *************************************************)
 
-lemma cir_lift: â\88\80G,K,T. â¦\83G, Kâ¦\84 â\8a¢ â\9e¡ ð\9d\90\88â¦\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 cir_lift: â\88\80G,K,T. â¦\83G, Kâ¦\84 â\8a¢ â\9e¡ ð\9d\90\88â¦\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⦄.
 /3 width=8 by crr_inv_lift/ qed.
 
-lemma cir_inv_lift: â\88\80G,L,U. â¦\83G, Lâ¦\84 â\8a¢ â\9e¡ ð\9d\90\88â¦\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 cir_inv_lift: â\88\80G,L,U. â¦\83G, Lâ¦\84 â\8a¢ â\9e¡ ð\9d\90\88â¦\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⦄.
 /3 width=8 by crr_lift/ qed-.