proposition: Lemma union_idempotent x : Equal (union x x) x.
proof: Proof. fsetdec. Qed.
imports: Coq.MSets.MSetInterface Coq.MSets.MSetProperties Coq.MSets.MSetFacts Coq.MSets.MSetDecide Fiat.Common.Instances Fiat.Common.BoolFacts Fiat.Common