-lemma cpg_inv_appl1_simple: â\88\80c,h,G,L,V1,T1,U. â¦\83G, Lâ¦\84 â\8a¢ â\93\90V1.T1 â\9e¡[c, h] U → 𝐒⦃T1⦄ →
- â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ T1 â\9e¡[cT, h] T2 &
+lemma cpg_inv_appl1_simple: â\88\80c,h,G,L,V1,T1,U. â¦\83G, Lâ¦\84 â\8a¢ â\93\90V1.T1 â¬\88[c, h] U → 𝐒⦃T1⦄ →
+ â\88\83â\88\83cV,cT,V2,T2. â¦\83G, Lâ¦\84 â\8a¢ V1 â¬\88[cV, h] V2 & â¦\83G, Lâ¦\84 â\8a¢ T1 â¬\88[cT, h] T2 &