-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
+theorem dsubst_lift_le: ∀h,N,M,d1,d2. d2 ≤ d1 →
+ [d2 ↙ ↑[d1 - d2, h] N] ↑[d1 + 1, h] M = ↑[d1, h] [d2 ↙ N] M.
+#h #N #M elim M -M