update in ground static_2 basic_2 apps_2

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lsubr.ma
index 42fd64fa1888d311a14c6611fa4fea377521cea2..2e79ed6292db860fc076837c54f67dc1f1a62f47 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lsubr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lsubr.ma
@@ -24,7 +24,7 @@ lemma lsubr_cpx_trans (G): lsub_trans … (cpx G) lsubr.
 qed-.
 
 lemma cpx_bind_unit (G) (L):
-      â\88\80V1,V2. â\9dªG,Lâ\9d« ⊢ V1 ⬈ V2 →
-      â\88\80J,T1,T2. â\9dªG,L.â\93¤[J]â\9d« ⊢ T1 ⬈ T2 →
-      â\88\80p,I. â\9dªG,Lâ\9d« ⊢ ⓑ[p,I]V1.T1 ⬈ ⓑ[p,I]V2.T2.
+      â\88\80V1,V2. â\9d¨G,Lâ\9d© ⊢ V1 ⬈ V2 →
+      â\88\80J,T1,T2. â\9d¨G,L.â\93¤[J]â\9d© ⊢ T1 ⬈ T2 →
+      â\88\80p,I. â\9d¨G,Lâ\9d© ⊢ ⓑ[p,I]V1.T1 ⬈ ⓑ[p,I]V2.T2.
 /4 width=4 by lsubr_cpx_trans, cpx_bind, lsubr_unit/ qed.