update in static_2

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma
index 1a3d604e9ef226564349b4f8b4f0ba049b7b80c4..c052a3a3c09a0be9e13606f4b38b80260391d643 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma
@@ -59,12 +59,12 @@ qed-.
 (* Basic_2A1: uses: fpbg_fleq_trans *)
 lemma fpbg_feqx_trans:
       ∀G1,G,L1,L,T1,T. ❪G1,L1,T1❫ > ❪G,L,T❫ →
-      â\88\80G2,L2,T2. â\9dªG,L,Tâ\9d« â\89\9b ❪G2,L2,T2❫ → ❪G1,L1,T1❫ > ❪G2,L2,T2❫.
+      â\88\80G2,L2,T2. â\9dªG,L,Tâ\9d« â\89\85 ❪G2,L2,T2❫ → ❪G1,L1,T1❫ > ❪G2,L2,T2❫.
 /3 width=5 by fpbg_fpbq_trans, fpbq_feqx/ qed-.
 
 (* Properties with t-bound rt-transition for terms **************************)
 
 lemma cpm_tneqx_cpm_fpbg (h) (G) (L):
-      â\88\80n1,T1,T. â\9dªG,Lâ\9d« â\8a¢ T1 â\9e¡[h,n1] T â\86\92 (T1 â\89\9b T → ⊥) →
+      â\88\80n1,T1,T. â\9dªG,Lâ\9d« â\8a¢ T1 â\9e¡[h,n1] T â\86\92 (T1 â\89\85 T → ⊥) →
       ∀n2,T2. ❪G,L❫ ⊢ T ➡[h,n2] T2 → ❪G,L,T1❫ > ❪G,L,T2❫.
 /4 width=5 by fpbq_fpbs, cpm_fpbq, cpm_fpb, ex2_3_intro/ qed.