(* *)
(**************************************************************************)
+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".
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.