X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Fcomputation%2Fcsn_lcpr.ma;h=98ee1843748ffedabb3571c06618a45f0449d9f9;hb=f21509c476b20e5446335c967b1e81f87ceb4f6c;hp=77ae2f9dbe2d2f0782176cde521a3d0e1efed1e5;hpb=16bbb2d6b16d5647d944f18f0fd6d4dd3df431fe;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lcpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lcpr.ma
index 77ae2f9db..98ee18437 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lcpr.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lcpr.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "Basic_2/grammar/tstc_tstc.ma".
 include "Basic_2/reducibility/lcpr_cpr.ma".
 include "Basic_2/computation/cprs_cprs.ma".
 include "Basic_2/computation/csn_lift.ma".
@@ -117,3 +118,30 @@ qed.
 lemma csn_appl_theta: ∀V1,V2. ⇧[0, 1] V1 ≡ V2 →
                       ∀L,V,T. L ⊢ ⬇* ⓓV. ⓐV2. T → L ⊢ ⬇* ⓐV1. ⓓV. T.
 /2 width=5/ qed.
+
+(* Basic_1: was only: sn3_appl_appl *)
+lemma csn_appl_simple_tstc: ∀L,V. L ⊢ ⬇* V → ∀T1.
+                            L ⊢ ⬇* T1 →
+                            (∀T2. L ⊢ T1 ➡* T2 → (T1 ≃ T2 → False) → L ⊢ ⬇* ⓐV. T2) →
+                            𝐒[T1] → L ⊢ ⬇* ⓐV. T1.
+#L #V #H @(csn_ind … H) -V #V #_ #IHV #T1 #H @(csn_ind … H) -T1 #T1 #H1T1 #IHT1 #H2T1 #H3T1
+@csn_intro #X #HL #H
+elim (cpr_inv_appl1_simple … HL ?) -HL //
+#V0 #T0 #HLV0 #HLT10 #H0 destruct
+elim (eq_false_inv_tpair_sn … H) -H
+[ -IHT1 #HV0
+  @(csn_cpr_trans … (ⓐV0.T1)) /2 width=1/ -HLT10
+  @IHV -IHV // -H1T1 -H3T1 /2 width=1/ -HV0
+  #T2 #HLT12 #HT12
+  @(csn_cpr_trans … (ⓐV.T2)) /2 width=1/ -HLV0
+  @H2T1 -H2T1 // -HLT12 /2 width=1/
+| -IHV -H1T1 -HLV0 * #H #H1T10 destruct
+  elim (tstc_dec T1 T0) #H2T10
+  [ @IHT1 -IHT1 // /2 width=1/ -H1T10 /2 width=3/ -H3T1
+    #T2 #HLT02 #HT02
+    @H2T1 -H2T1 /2 width=3/ -HLT10 -HLT02 /3 width=3/
+  | -IHT1 -H3T1 -H1T10
+    @H2T1 -H2T1 /2 width=1/
+  ]
+]
+qed.