-
-(* 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.