X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fetc%2Fcpxs%2Fcpxs.etc;h=ada873d816ad1e18da99ed75d40c21108da0808a;hb=10b733131aa2667d8ba4318d517f0ba3cf137359;hp=89e1466f7ae7dec0b78d728a50e2c2b0cc910df2;hpb=06531086fc492d0fd374ada30e116b56a5eff957;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpxs/cpxs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpxs/cpxs.etc
index 89e1466f7..ada873d81 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/cpxs/cpxs.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpxs/cpxs.etc
@@ -7,8 +7,7 @@ lemma cprs_cpxs: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈* T2 → ⦃G, L⦄ ⊢
 cpr_cpx/
 qed.
 
-lemma cpxs_inv_cnx1: ∀h,o,G,L,T,U. ⦃G, L⦄ ⊢ T ⬈*[h] U → ⦃G, L⦄ ⊢ ⬈[h]
-𝐍⦃T⦄ → T = U.
+lemma cpxs_inv_cnx1: ∀h,o,G,L,T,U. ⦃G, L⦄ ⊢ T ⬈*[h] U → ⦃G, L⦄ ⊢ ⬈[h] 𝐍⦃T⦄ → T = U.
 #h #o #G #L #T #U #H @(cpxs_ind_dx … H) -T //
 #T0 #T #H1T0 #_ #IHT #H2T0
 lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1 by/