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

diff --git a/matita/matita/contribs/lambda/multiplicity.ma b/matita/matita/contribs/lambda/multiplicity.ma
index d6d5af110..040f1c67b 100644
--- a/matita/matita/contribs/lambda/multiplicity.ma
+++ b/matita/matita/contribs/lambda/multiplicity.ma
@@ -23,11 +23,11 @@ let rec mult M on M ≝ match M with
 | Appl B A ⇒ (mult B) + (mult A)
 ].
 
-interpretation "multiplicity"
+interpretation "term multiplicity"
    'Multiplicity M = (mult M).
 
-notation "hvbox( #{M} )"
-   non associative with precedence 55
+notation "hvbox( #{ term 46 M } )"
+   non associative with precedence 90
    for @{ 'Multiplicity $M }.
 
 lemma mult_positive: ∀M. 0 < #{M}.
@@ -35,11 +35,11 @@ lemma mult_positive: ∀M. 0 < #{M}.
 qed.
 
 lemma mult_lift: ∀h,M,d. #{↑[d, h] M} = #{M}.
-#H #M elim M -M normalize //
+#h #M elim M -M normalize //
 qed.
 
-theorem mult_dsubst: ∀C,M,d. #{[d ⬐ C] M} ≤ #{M} * #{C}.
-#C #M elim M -M
+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 //
   | destruct >dsubst_vref_eq normalize //