| 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}.
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 //