lemma csx_appl_simple (G) (L):
∀V. ❪G,L❫ ⊢ ⬈*𝐒 V → ∀T1.
- (â\88\80T2. â\9dªG,Lâ\9d« â\8a¢ T1 â¬\88 T2 â\86\92 (T1 â\89\9b T2 → ⊥) → ❪G,L❫ ⊢ ⬈*𝐒 ⓐV.T2) →
+ (â\88\80T2. â\9dªG,Lâ\9d« â\8a¢ T1 â¬\88 T2 â\86\92 (T1 â\89\85 T2 → ⊥) → ❪G,L❫ ⊢ ⬈*𝐒 ⓐV.T2) →
𝐒❪T1❫ → ❪G,L❫ ⊢ ⬈*𝐒 ⓐV.T1.
#G #L #V #H @(csx_ind … H) -V
#V #_ #IHV #T1 #IHT1 #HT1