update in basic_2

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

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 cd6c84688aafe405ad46f579b6081fd7a15bec2d..b71b21075b1af4f945336d001da1c1f9deffbb6f 100644 (file)
--- 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-.