proposition: Corollary Union_add_l {X : Type} (A B : Ensemble X) (x : X) : Add (Union A B) x = Union (Add A x) B.
proof: Proof. rewrite (Union_commutative _ (Add _ _)). rewrite <- (Union_add_r _ _ A). rewrite (Union_commutative _ B). reflexivity. Qed.
imports: ZornsLemma(FunctionProperties) Coq(RelationClasses)