X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Fcomputation%2Fcsn_lift.ma;h=1326a8bb482d556adf75daa324d495250180b580;hb=44c1079dabf1d3c0b69d0155ddbaea8627ec901c;hp=de29660f091fce6b658cd481f0722119643c3c41;hpb=16bbb2d6b16d5647d944f18f0fd6d4dd3df431fe;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lift.ma
index de29660f0..1326a8bb4 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lift.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lift.ma
@@ -78,7 +78,6 @@ elim (eq_false_inv_tpair_sn … H2) -H2
 ]
 qed.
 
-(* Basic_1: was only: sn3_appl_appl *)
 lemma csn_appl_simple: ∀L,V. L ⊢ ⬇* V → ∀T1.
                        (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → False) → L ⊢ ⬇* ⓐV. T2) →
                        𝐒[T1] → L ⊢ ⬇* ⓐV. T1.
@@ -92,19 +91,8 @@ elim (eq_false_inv_tpair_dx … H2) -H2
   @IHT1 -IHT1 // /2 width=1/
 | -HLT10 * #H #HV0 destruct
   @IHV -IHV // -HT1 /2 width=1/ -HV0
-  #T2 #HLT02 #HT02 
+  #T2 #HLT02 #HT02
   @(csn_cpr_trans … (ⓐV.T2)) /2 width=1/ -HLV0
   @IHT1 -IHT1 // -HLT02 /2 width=1/
 ]
 qed.
-
-(* Basic_1: was only: sn3_appl_appls *)
-lemma csn_appl_appls_simple: ∀L,V. L ⊢ ⬇* V → ∀Vs,T1.
-                             (∀T2. L ⊢ ⒶVs.T1 ➡ T2 → (ⒶVs.T1 = T2 → False) → L ⊢ ⬇* ⓐV. T2) →
-                             𝐒[T1] → L ⊢ ⬇* ⓐV. ⒶVs. T1.
-#L #V #HV #Vs elim Vs -Vs
-[ @csn_appl_simple //
-| #V0 #Vs #_ #T1 #HT1 #_
-  @csn_appl_simple // -HV @HT1
-]
-qed.