-lemma cpxs_inv_abbr1_dx (h) (p) (G) (L):
- â\88\80V1,T1,U2. â\9dªG,Lâ\9d« â\8a¢ â\93\93[p]V1.T1 â¬\88*[h] U2 →
- â\88¨â\88¨ â\88\83â\88\83V2,T2. â\9dªG,Lâ\9d« â\8a¢ V1 â¬\88*[h] V2 & â\9dªG,L.â\93\93V1â\9d« â\8a¢ T1 â¬\88*[h] T2 & U2 = ⓓ[p]V2.T2
- | â\88\83â\88\83T2. â\9dªG,L.â\93\93V1â\9d« â\8a¢ T1 â¬\88*[h] T2 & ⇧[1] U2 ≘ T2 & p = Ⓣ.
-#h #p #G #L #V1 #T1 #U2 #H
+lemma cpxs_inv_abbr1_dx (p) (G) (L):
+ â\88\80V1,T1,U2. â\9d¨G,Lâ\9d© â\8a¢ â\93\93[p]V1.T1 â¬\88* U2 →
+ â\88¨â\88¨ â\88\83â\88\83V2,T2. â\9d¨G,Lâ\9d© â\8a¢ V1 â¬\88* V2 & â\9d¨G,L.â\93\93V1â\9d© â\8a¢ T1 â¬\88* T2 & U2 = ⓓ[p]V2.T2
+ | â\88\83â\88\83T2. â\9d¨G,L.â\93\93V1â\9d© â\8a¢ T1 â¬\88* T2 & ⇧[1] U2 ≘ T2 & p = Ⓣ.
+#p #G #L #V1 #T1 #U2 #H