-elim (cpr_inv_abst1 … H1 I V) -H1
-#W0 #T0 #HLW0 #HLT0 #H destruct
-elim (eq_false_inv_tpair_sn … H2) -H2
-[ /3 width=5/
-| -HLW0 * #H destruct /3 width=1/
-]
-qed.
-
-lemma csn_appl_simple: ∀L,V. L ⊢ ⬊* V → ∀T1.
- (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → L ⊢ ⬊* ⓐV. T2) →
- 𝐒⦃T1⦄ → L ⊢ ⬊* ⓐV. T1.
-#L #V #H @(csn_ind … H) -V #V #_ #IHV #T1 #IHT1 #HT1
-@csn_intro #X #H1 #H2
-elim (cpr_inv_appl1_simple … H1 ?) // -H1