update in ground_2, static_2, basic_2, apps_2, alpha_1

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_transition / cnx_basic.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_basic.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_basic.ma
index 4f07b3e5e3cce58c1186aeb8dd42c130d13c61dc..41cb6dad884cb758007a1bf1b5f6e2c7a8219fa8 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_basic.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_basic.ma
@@ -20,7 +20,7 @@ include "basic_2/rt_transition/cnx.ma".
 
 (* Advanced inversion lemmas ************************************************)
 
-lemma cnx_inv_abbr_pos (h) (G) (L): â\88\80V,T.  â¦\83G,Lâ¦\84 â\8a¢ â¬\88[h] ð\9d\90\8dâ¦\83+â\93\93V.Tâ¦\84 → ⊥.
+lemma cnx_inv_abbr_pos (h) (G) (L): â\88\80V,T.  â\9dªG,Lâ\9d« â\8a¢ â¬\88[h] ð\9d\90\8dâ\9dª+â\93\93V.Tâ\9d« → ⊥.
 #h #G #L #V #U1 #H
 elim (cpx_subst h G (L.ⓓV) U1 … 0) [|*: /2 width=4 by drops_refl/ ] #U2 #T2 #HU12 #HTU2
 elim (teqx_dec U1 U2) #HnU12 [ -HU12 | -HTU2 ]