update in basic_2 and ground_2

[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 98d617600407b05ebe58dea804a1b6c5407ad145..702ca5ab992e29ee0cedf060872dc80aa6abfbdd 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,o,G,K,T. â¦\83G, Kâ¦\84 â\8a¢ T ¡[h, o] â\86\92 â\88\80L,b,l,k. â¬\87[b, l, k] L â\89¡ K →
-                â\88\80U. â¬\86[l, k] T â\89¡ U → ⦃G, L⦄ ⊢ U ¡[h, o].
+lemma snv_lift: â\88\80h,o,G,K,T. â¦\83G, Kâ¦\84 â\8a¢ T ¡[h, o] â\86\92 â\88\80L,b,l,k. â¬\87[b, l, k] L â\89\98 K →
+                â\88\80U. â¬\86[l, k] T â\89\98 U → ⦃G, L⦄ ⊢ U ¡[h, o].
 #h #o #G #K #T #H elim H -G -K -T
 [ #G #K #s #L #b #l #k #_ #X #H
   >(lift_inv_sort1 … H) -X -K -l -k //
@@ -48,8 +48,8 @@ lemma snv_lift: ∀h,o,G,K,T. ⦃G, K⦄ ⊢ T ¡[h, o] → ∀L,b,l,k. ⬇[b, l
 ]
 qed.
 
-lemma snv_inv_lift: â\88\80h,o,G,L,U. â¦\83G, Lâ¦\84 â\8a¢ U ¡[h, o] â\86\92 â\88\80K,b,l,k. â¬\87[b, l, k] L â\89¡ K →
-                    â\88\80T. â¬\86[l, k] T â\89¡ U → ⦃G, K⦄ ⊢ T ¡[h, o].
+lemma snv_inv_lift: â\88\80h,o,G,L,U. â¦\83G, Lâ¦\84 â\8a¢ U ¡[h, o] â\86\92 â\88\80K,b,l,k. â¬\87[b, l, k] L â\89\98 K →
+                    â\88\80T. â¬\86[l, k] T â\89\98 U → ⦃G, K⦄ ⊢ T ¡[h, o].
 #h #o #G #L #U #H elim H -G -L -U
 [ #G #L #s #K #b #l #k #_ #X #H
   >(lift_inv_sort2 … H) -X -L -l -k //