-lemma slift_inv_appl: ∀b0,W,U,d,h,E. ↑[d, h] E = {b0}@W.U →
- ∃∃V,T. ↑[d, h] V = W & ↑[d, h] T = U & E = {b0}@V.T.
-#b0 #W #U #d #h * normalize
+lemma slift_inv_appl: ∀c,W,U,d,h,E. ↑[d, h] E = {c}@W.U →
+ ∃∃V,T. ↑[d, h] V = W & ↑[d, h] T = U & E = {c}@V.T.
+#c #W #U #d #h * normalize