proposition: Lemma permut_get_2 : forall l1 l2 l3, (l1 \u l2 \u l3) = (l2 \u l1 \u l3).
proof: Proof. Proof using. intros. apply union_comm_assoc. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibRelation LibList LibInt LibNat LibOperation LibEpsilon LibSet LibMonoid)