include "lambda/terms/relocating_substitution.ma".
+include "lambda/notation/functions/multiplicity_1.ma".
+
(* MULTIPLICITY *************************************************************)
(* Note: this gives the number of variable references in M *)
interpretation "term multiplicity"
'Multiplicity M = (mult M).
-notation "hvbox( ♯{ term 46 M } )"
- non associative with precedence 90
- for @{ 'Multiplicity $M }.
-
lemma mult_positive: ∀M. 0 < ♯{M}.
#M elim M -M // /2 width=1/
qed.