# let [MULTISAME_REFL;MULTISAME_SYM;MULTISAME_TRANS] = (CONJUNCTS o prove)
(`(!l:(A)list. multisame l l) /\
(!l l':(A)list. multisame l l' <=> multisame l' l) /\
(!l1 l2 l3:(A)list.
multisame l1 l2 /\ multisame l2 l3 ==> multisame l1 l3)`,
REWRITE_TAC[multisame] THEN MESON_TAC[]);;
and can now lift theorems. For example, we know that # let [MULTIPLICITY_MUNION;MUNION_ASSOC] =
map (lift_theorem (multiset_abs,multiset_rep)
(MULTISAME_REFL,MULTISAME_SYM,MULTISAME_TRANS)
[multiplicity_th; munion_th])
[LISTMULT_APPEND; MULTISAME_APPEND_ASSOC];;
val ( MULTIPLICITY_MUNION ) : thm =
|- !a l m.
multiplicity a (munion l m) = multiplicity a l + multiplicity a m
val ( MUNION_ASSOC ) : thm =
|- !l m n. munion l (munion m n) = munion (munion l m) n