proposition: Lemma permut_tactic_keep : forall C l1 l2 l3 l4, C ((l1 \u l2) \u l3) l4 -> C (l1 \u (l2 \u l3)) l4.
proof: Proof. Proof using. intros. rews_permut_simpl. eauto. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibRelation LibList LibInt LibNat LibOperation LibEpsilon LibSet LibMonoid)