X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcpxs_teqo.ma;h=b71b21075b1af4f945336d001da1c1f9deffbb6f;hb=57ae1762497a5f3ea75740e2908e04adb8642cc2;hp=cd6c84688aafe405ad46f579b6081fd7a15bec2d;hpb=ca7327c20c6031829fade8bb84a3a1bb66113f54;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqo.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqo.ma
index cd6c84688..b71b21075 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqo.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_teqo.ma
@@ -97,6 +97,6 @@ elim (cpxs_inv_cast1 … H) -H /2 width=1 by or3_intro1, or3_intro2/ *
 qed-.
 
 lemma cpxs_fwd_cnx (h) (G) (L):
-      ∀T1. ❪G,L❫ ⊢ ⬈[h] 𝐍❪T1❫ →
+      ∀T1. ❪G,L❫ ⊢ ⬈𝐍[h] T1 →
       ∀X2. ❪G,L❫ ⊢ T1 ⬈*[h] X2 → T1 ⩳ X2.
 /3 width=5 by cpxs_inv_cnx1, teqx_teqo/ qed-.