X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcpxs_cnx.ma;h=6dd8020012ed4fcf26379ff10596ba1763ea656b;hp=2135a0cee8b5b81cfb38b1f16067279deac891cb;hb=f308429a0fde273605a2330efc63268b4ac36c99;hpb=87f57ddc367303c33e19c83cd8989cd561f3185b

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_cnx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_cnx.ma
index 2135a0cee..6dd802001 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_cnx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_cnx.ma
@@ -19,7 +19,7 @@ include "basic_2/rt_computation/cpxs.ma".
 
 (* Inversion lemmas with normal terms ***************************************)
 
-lemma cpxs_inv_cnx1: ∀h,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → ⦃G, L⦄ ⊢ ⬈[h] 𝐍⦃T1⦄ →
+lemma cpxs_inv_cnx1: ∀h,G,L,T1,T2. ⦃G,L⦄ ⊢ T1 ⬈*[h] T2 → ⦃G,L⦄ ⊢ ⬈[h] 𝐍⦃T1⦄ →
                      T1 ≛ T2.
 #h #G #L #T1 #T2 #H @(cpxs_ind_dx … H) -T1
 /5 width=9 by cnx_tdeq_trans, tdeq_trans/