proposition: Lemma demo_multiset_union_permut_simpl_3 : forall (x y:A) l1 l1' l2 l3 l4, l1 \c l4 \u l1' -> (l1 \u (\{x} \u l2) \u \{x} \u (\{y} \u l3)) \c (\{y} \u \{x} \u (l1' \u l2 \u l4) \u (\{x} \u l3)).
proof: Proof. Proof using. intros. dup. permut_simpl_prepare. permut_simpl_once. permut_simpl_once. permut_simpl_once. permut_simpl_once. permut_simpl_once. permut_simpl_once. try permut_simpl_once. rew_permut_simpl. equates 1. apply H. permut_simpl_prepare. permut_simpl_once. rew_permut_simpl. permut_conclude. permut_simpl. applys_eq H. permut_simpl. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibRelation LibList LibInt LibNat LibOperation LibEpsilon LibSet LibMonoid)