X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda%2Fmultiplicity.ma;fp=matita%2Fmatita%2Fcontribs%2Flambda%2Fmultiplicity.ma;h=4f91a63089d5178a4805e08dd9aed18daed80781;hb=5ca47b58902b9f2583ad1354b860c04ea62df46c;hp=040f1c67b5f1a0f1b0a8f6a58b8a23939adc1f24;hpb=2199f327081f49b21bdcd23d702b5e07ea4f58ce;p=helm.git

diff --git a/matita/matita/contribs/lambda/multiplicity.ma b/matita/matita/contribs/lambda/multiplicity.ma
index 040f1c67b..4f91a6308 100644
--- a/matita/matita/contribs/lambda/multiplicity.ma
+++ b/matita/matita/contribs/lambda/multiplicity.ma
@@ -38,7 +38,7 @@ lemma mult_lift: ∀h,M,d. #{↑[d, h] M} = #{M}.
 #h #M elim M -M normalize //
 qed.
 
-theorem mult_dsubst: ∀D,M,d. #{[d ⬐ D] M} ≤ #{M} * #{D}.
+theorem mult_dsubst: ∀D,M,d. #{[d ↙ 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 //