update in ground static_2 basic_2 apps_2

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_fsle.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_fsle.ma
index d7e5e89ea11d5b3bd6059a0a5edcb0978c082c58..5eed0ea7acd240a7b6be802ec8d73af0d928b509 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_fsle.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_fsle.ma
@@ -22,12 +22,12 @@ include "basic_2/rt_transition/rpx_fqup.ma".
 
 (* Forward lemmas with free variables inclusion for restricted closures *****)
 
-(* Note: "â\9dªL2, T1â\9d« â\8a\86 â\9dªL2, T0â\9d«" does not hold *)
+(* Note: "â\9d¨L2, T1â\9d© â\8a\86 â\9d¨L2, T0â\9d©" does not hold *)
 (* Note: Take L0 = K0.ⓓ(ⓝW.V), L2 = K0.ⓓW, T0 = #0, T1 = ⇧[1]V *)
 (* Note: This invalidates rpxs_cpx_conf: "∀G. s_r_confluent1 … (cpx G) (rpxs G)" *)
 lemma rpx_cpx_conf_fsge (G):
-      â\88\80L0,T0,T1. â\9dªG,L0â\9d« ⊢ T0 ⬈ T1 →
-      â\88\80L2. â\9dªG,L0â\9d« â\8a¢â¬\88[T0] 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[T0] L2 â\86\92 â\9d¨L2,T1â\9d© â\8a\86 â\9d¨L0,T0â\9d©.
 #G0 #L0 #T0 @(fqup_wf_ind_eq (Ⓣ) … G0 L0 T0) -G0 -L0 -T0
 #G #L #T #IH #G0 #L0 * *
 [ #s0 #HG #HL #HT #X #HX #Y #HY destruct -IH
@@ -135,6 +135,6 @@ lemma rpx_cpx_conf_sn (G): s_r_confluent1 … (cpx G) (rpx G).
 /2 width=5 by cpx_rex_conf_sn/ qed-.
 
 lemma rpx_cpx_conf_fsge_dx (G):
-      â\88\80L0,T0,T1. â\9dªG,L0â\9d« ⊢ T0 ⬈ T1 →
-      â\88\80L2. â\9dªG,L0â\9d« â\8a¢â¬\88[T0] L2 â\86\92 â\9dªL2,T1â\9d« â\8a\86 â\9dªL0,T1â\9d«.
+      â\88\80L0,T0,T1. â\9d¨G,L0â\9d© ⊢ T0 ⬈ T1 →
+      â\88\80L2. â\9d¨G,L0â\9d© â\8a¢â¬\88[T0] L2 â\86\92 â\9d¨L2,T1â\9d© â\8a\86 â\9d¨L0,T1â\9d©.
 /3 width=5 by rpx_cpx_conf_sn, rpx_fsge_comp/ qed-.