proposition: Lemma mult_insert : forall r l l' h, mult (transp r) l l' -> mult (transp r) (h :: l) (h :: l').
proof: Proof. intros r l l' h Hm. unfold mult,MultisetLT, transp in *; simpl. inversion Hm. constructor 1 with (X := X) (Y := Y) (Z := insert h Z); auto with multisets. rewrite H0; try_solve_meq. rewrite H1; try_solve_meq. Qed.
imports: Coq(List Permutation Arith Morphisms Basics) CoLoR(MultisetOrder RelExtras MultisetCore MultisetList MultisetTheory AccUtil RelUtil LogicUtil) CoLoR(AccUtil ListUtil)