proposition: Lemma demo_multiset_union_permut_simpl_2 : forall (x:A) l1 l2 l3 l4, (l1 \u \{x} \u l3 \u l2) \c (l1 \u l2 \u l4 \u (\{x} \u l3)).
proof: Proof. Proof using. intros. permut_simpl_prepare. permut_simpl_once. permut_simpl_once. permut_simpl_once. permut_simpl_once. rew_permut_simpl. permut_conclude. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibRelation LibList LibInt LibNat LibOperation LibEpsilon LibSet LibMonoid)