-theorem dsubst_lift_le: ∀h,C,M,d1,d2. d2 ≤ d1 →
- [d2 ⬐ ↑[d1 - d2, h] C] ↑[d1 + 1, h] M = ↑[d1, h] [d2 ⬐ C] M.
-#h #C #M elim M -M
+theorem dsubst_lift_le: ∀h,D,M,d1,d2. d2 ≤ d1 →
+ [d2 ⬐ ↑[d1 - d2, h] D] ↑[d1 + 1, h] M = ↑[d1, h] [d2 ⬐ D] M.
+#h #D #M elim M -M