X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fcomputation%2Fcsn_cprs.ma;h=c32947631c92ef7d6512d20109905835f9233f76;hb=e0827239f4b44f2af9c7f88c4c7c41f2a193ae37;hp=530fde74c2271de0fef1592f602df1aa7cb5cd16;hpb=70e6a24c9505c950714f138506f3eedb293084c5;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_cprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_cprs.ma
index 530fde74c..c32947631 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_cprs.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_cprs.ma
@@ -88,17 +88,6 @@ qed.
 lemma csn_cprs_trans: ∀L,T1. L ⊢ ⬇* T1 → ∀T2. L ⊢ T1 ➡* T2 → L ⊢ ⬇* T2.
 /4 width=3/ qed.
 
-(* Basic_1: was: nf2_sn3 *)
-lemma csn_cwn: ∀L,T1. L ⊢ ⬇* T1 →
-               ∃∃T2. L ⊢ T1 ➡* T2 & L ⊢ 𝐍[T2].
-#L #T1 #H elim H -T1 #T1 #_ #IHT1
-elim (cnf_dec L T1)
-[ -IHT1 /2 width=3/
-| * #T2 #HLT12 #HT12
-  elim (IHT1 T2 ? ?) -IHT1 // /2 width=1/ -HT12 /3 width=3/
-]
-qed.
-
 (* Main eliminators *********************************************************)
 
 lemma csn_ind_cprs: ∀L. ∀R:predicate term.