#h #M elim M -M normalize //
qed.
-theorem mult_dsubst: â\88\80D,M,d. #{[d â¬\90 D] M} ≤ #{M} * #{D}.
+theorem mult_dsubst: â\88\80D,M,d. #{[d â\86\99 D] M} ≤ #{M} * #{D}.
#D #M elim M -M
[ #i #d elim (lt_or_eq_or_gt i d) #Hid
[ >(dsubst_vref_lt … Hid) normalize //