update in ground static_2 basic_2 apps_2

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_fsle.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_fsle.ma
index 14a30512fd2149db2f61405b78020931a3d703f3..77868539ba836cb836917cdf86c4f3c721335897 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_fsle.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_fsle.ma
@@ -20,11 +20,11 @@ include "basic_2/rt_transition/rpx_lpx.ma".
 
 (* Basic_2A1: uses: lpx_cpx_frees_trans *)
 lemma lpx_cpx_conf_fsge (G):
-      â\88\80L0,T0,T1. â\9dªG,L0â\9d« ⊢ T0 ⬈ T1 →
-      â\88\80L2. â\9dªG,L0â\9d« â\8a¢ â¬\88 L2 â\86\92 â\9dªL2,T1â\9d« â\8a\86 â\9dªL0,T0â\9d«.
+      â\88\80L0,T0,T1. â\9d¨G,L0â\9d© ⊢ T0 ⬈ T1 →
+      â\88\80L2. â\9d¨G,L0â\9d© â\8a¢ â¬\88 L2 â\86\92 â\9d¨L2,T1â\9d© â\8a\86 â\9d¨L0,T0â\9d©.
 /3 width=4 by rpx_cpx_conf_fsge, lpx_rpx/ qed-.
 
 (* Basic_2A1: uses: lpx_frees_trans *)
 lemma lpx_fsge_comp (G):
-      â\88\80L0,L2,T0. â\9dªG,L0â\9d« â\8a¢ â¬\88 L2 â\86\92 â\9dªL2,T0â\9d« â\8a\86 â\9dªL0,T0â\9d«.
+      â\88\80L0,L2,T0. â\9d¨G,L0â\9d© â\8a¢ â¬\88 L2 â\86\92 â\9d¨L2,T0â\9d© â\8a\86 â\9d¨L0,T0â\9d©.
 /2 width=4 by lpx_cpx_conf_fsge/ qed-.