-lemma csx_appl_simple: â\88\80h,G,L,V. â¦\83G,Lâ¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83Vâ¦\84 → ∀T1.
- (â\88\80T2. â¦\83G,Lâ¦\84 â\8a¢ T1 â¬\88[h] T2 â\86\92 (T1 â\89\9b T2 â\86\92 â\8a¥) â\86\92 â¦\83G,Lâ¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83â\93\90V.T2â¦\84) →
- ð\9d\90\92â¦\83T1â¦\84 â\86\92 â¦\83G,Lâ¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83â\93\90V.T1â¦\84.
+lemma csx_appl_simple: â\88\80h,G,L,V. â\9dªG,Lâ\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªVâ\9d« → ∀T1.
+ (â\88\80T2. â\9dªG,Lâ\9d« â\8a¢ T1 â¬\88[h] T2 â\86\92 (T1 â\89\9b T2 â\86\92 â\8a¥) â\86\92 â\9dªG,Lâ\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªâ\93\90V.T2â\9d«) →
+ ð\9d\90\92â\9dªT1â\9d« â\86\92 â\9dªG,Lâ\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªâ\93\90V.T1â\9d«.