update in static_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / fpbs_cpxs.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpxs.ma
index ec9cf1bb57e49d51f0dea0fa36f7945adf5cd64b..f9d110dd114aca54e9d5d8456e94480abf596319 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpxs.ma
@@ -40,14 +40,14 @@ lemma cpxs_fpbs_trans:
 qed-.
 
 lemma cpxs_teqx_fpbs_trans:
-      â\88\80G1,L1,T1,T. â\9dªG1,L1â\9d« â\8a¢ T1 â¬\88* T â\86\92 â\88\80T0. T â\89\9b T0 →
+      â\88\80G1,L1,T1,T. â\9dªG1,L1â\9d« â\8a¢ T1 â¬\88* T â\86\92 â\88\80T0. T â\89\85 T0 →
       ∀G2,L2,T2. ❪G1,L1,T0❫ ≥ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫.
 /3 width=3 by cpxs_fpbs_trans, teqx_fpbs_trans/ qed-.
 
 lemma cpxs_teqx_fpbs:
       ∀G,L,T1,T. ❪G,L❫ ⊢ T1 ⬈* T →
-      â\88\80T2. T â\89\9b T2 → ❪G,L,T1❫ ≥ ❪G,L,T2❫.
-/4 width=3 by cpxs_fpbs_trans, feqx_fpbs, teqx_feqx/ qed.
+      â\88\80T2. T â\89\85 T2 → ❪G,L,T1❫ ≥ ❪G,L,T2❫.
+/4 width=3 by cpxs_fpbs_trans, feqx_fpbs, teqg_feqg/ qed.
 
 (* Properties with star-iterated structural successor for closures **********)