notational change for snv and lsubsv: inverted "!" used for now

[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 ec9be23a4521e5cca5484f4f3c98084b51ccf5cd..854fff7f3448b57640bd4ed09cb613c94afa444e 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,K,T. â¦\83h, Kâ¦\84 â\8a© T :[g] → ∀L,d,e. ⇩[d, e] L ≡ K →
-                â\88\80U. â\87§[d, e] T â\89¡ U â\86\92 â¦\83h, Lâ¦\84 â\8a© U :[g].
+lemma snv_lift: â\88\80h,g,K,T. â¦\83h, Kâ¦\84 â\8a¢ T ¡[g] → ∀L,d,e. ⇩[d, e] L ≡ K →
+                â\88\80U. â\87§[d, e] T â\89¡ U â\86\92 â¦\83h, Lâ¦\84 â\8a¢ U ¡[g].
 #h #g #K #T #H elim H -K -T
 [ #K #k #L #d #e #_ #X #H
   >(lift_inv_sort1 … H) -X -K -d -e //
@@ -50,8 +50,8 @@ lemma snv_lift: ∀h,g,K,T. ⦃h, K⦄ ⊩ T :[g] → ∀L,d,e. ⇩[d, e] L ≡
 ]
 qed.
 
-lemma snv_inv_lift: â\88\80h,g,L,U. â¦\83h, Lâ¦\84 â\8a© U :[g] → ∀K,d,e. ⇩[d, e] L ≡ K →
-                    â\88\80T. â\87§[d, e] T â\89¡ U â\86\92 â¦\83h, Kâ¦\84 â\8a© T :[g].
+lemma snv_inv_lift: â\88\80h,g,L,U. â¦\83h, Lâ¦\84 â\8a¢ U ¡[g] → ∀K,d,e. ⇩[d, e] L ≡ K →
+                    â\88\80T. â\87§[d, e] T â\89¡ U â\86\92 â¦\83h, Kâ¦\84 â\8a¢ T ¡[g].
 #h #g #L #U #H elim H -L -U
 [ #L #k #K #d #e #_ #X #H
   >(lift_inv_sort2 … H) -X -L -d -e //