X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fetc%2Fcprs%2Fcprs.etc;h=b20ba8ff81d54de03a5c2a7339dd379f87ebe831;hp=a51dba5d671847a033dacb2c67bed6de536f49ed;hb=dd93a0919b67bead0d4f07d49dfc198006edc9aa;hpb=4173283e148199871d787c53c0301891deb90713

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cprs/cprs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cprs/cprs.etc
index a51dba5d6..b20ba8ff8 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/cprs/cprs.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cprs/cprs.etc
@@ -1,10 +1,3 @@
 (* Basic_1: was: pr3_pr1 *)
 lemma tprs_cprs: ∀G,L,T1,T2. ⦃G, ⋆⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ T1 ➡* T2.
 /2 width=3 by lsubr_cprs_trans/ qed.
-
-(* Basic_1: was: nf2_pr3_unfold *)
-lemma cprs_inv_cnr1: ∀G,L,T,U. ⦃G, L⦄ ⊢ T ➡* U → ⦃G, L⦄ ⊢ ➡ 𝐍⦃T⦄ → T = U.
-#G #L #T #U #H @(cprs_ind_dx … H) -T //
-#T0 #T #H1T0 #_ #IHT #H2T0
-lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1 by/
-qed-.