update in ground_2 static_2 basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / etc / cprs / cprs.etc

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 a51dba5d671847a033dacb2c67bed6de536f49ed..b20ba8ff81d54de03a5c2a7339dd379f87ebe831 100644 (file)
--- 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-.