-lemma cpxs_fwd_delta_drops (h) (I) (G) (L) (K):
- ∀V1,i. ⇩*[i] L ≘ K.ⓑ{I}V1 →
- ∀V2. ⇧*[↑i] V1 ≘ V2 →
- â\88\80X2. â¦\83G,Lâ¦\84 â\8a¢ #i â¬\88*[h] X2 →
- â\88¨â\88¨ #i ⩳ X2 | â¦\83G,Lâ¦\84 â\8a¢ V2 â¬\88*[h] X2.
-#h #I #G #L #K #V1 #i #HLK #V2 #HV12 #X2 #H
+lemma cpxs_fwd_delta_drops (I) (G) (L) (K):
+ ∀V1,i. ⇩[i] L ≘ K.ⓑ[I]V1 →
+ ∀V2. ⇧[↑i] V1 ≘ V2 →
+ â\88\80X2. â\9dªG,Lâ\9d« â\8a¢ #i â¬\88* X2 →
+ â\88¨â\88¨ #i ⩳ X2 | â\9dªG,Lâ\9d« â\8a¢ V2 â¬\88* X2.
+#I #G #L #K #V1 #i #HLK #V2 #HV12 #X2 #H