update in static_2

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fqup.ma
index 71451e88698309a1a512ffe9b23f0476d49d7b0f..7acceab10134ebc9ccb84d48159e62d9254fa6f8 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fqup.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fqup.ma
@@ -21,8 +21,8 @@ include "basic_2/rt_computation/fpbg.ma".
 
 lemma fpbg_teqx_div:
       ∀G1,G2,L1,L2,T1,T. ❪G1,L1,T1❫ > ❪G2,L2,T❫ →
-      â\88\80T2. T2 â\89\9b T → ❪G1,L1,T1❫ > ❪G2,L2,T2❫.
-/4 width=5 by fpbg_feqx_trans, teqx_feqx, teqx_sym/ qed-.
+      â\88\80T2. T2 â\89\85 T → ❪G1,L1,T1❫ > ❪G2,L2,T2❫.
+/4 width=5 by fpbg_feqx_trans, teqg_feqg, teqx_sym/ qed-.
 
 (* Properties with plus-iterated structural successor for closures **********)