(* *)
(**************************************************************************)
+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".
[ #V0 #V1 #T1 #HLV0 #HLV01 #HLT1 #H destruct
lapply (cpr_intro … HLV0 HLV01) -HLV01 #HLV1
lapply (ltpr_cpr_trans (L. ⓓV) … HLT1) /2 width=1/ -V0 #HLT1
- elim (eq_false_inv_tpair … H2) -H2
+ elim (eq_false_inv_tpair_sn … H2) -H2
[ #HV1 @IHV // /2 width=1/ -HV1
@(csn_lcpr_conf (L. ⓓV)) /2 width=1/ -HLV1 /2 width=3/
| -IHV -HLV1 * #H destruct /3 width=1/
elim (lift_total V0 0 1) #V5 #HV05
elim (term_eq_dec (ⓓV.ⓐV2.T) (ⓓV4.ⓐV5.T3))
[ -IHVT #H0 destruct
- elim (eq_false_inv_tpair … H) -H
+ elim (eq_false_inv_tpair_sn … H) -H
[ -HLV10 -HLV34 -HV3 -HLT3 -HVT
>(lift_inj … HV12 … HV05) -V5
#H elim (H ?) //
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.