(* This file is copied from RamifyCoq project. *)

Require Coq.Setoids.Setoid.
Require Import Coq.Classes.Morphisms.
Require Export Coq.Classes.Equivalence.
Require Export Coq.Sets.Ensembles.
Require Import Coq.Sets.Constructive_sets.
Require Import Logic.lib.Coqlib.

Lemma Full_set_spec: forall A (v: A), Full_set A v <-> True.
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: iff (Full_set A v) True *)
  split; intros; constructor.
Qed.

Lemma Empty_set_spec: forall A (v: A), Empty_set A v <-> False.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: iff (Empty_set A v) False *)
  split; intros [].
Qed.

Lemma Intersection_spec: forall A (v: A) P Q, Intersection _ P Q v <-> P v /\ Q v.
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  split; intros.
  + inversion H; auto.
  + constructor; tauto.
Qed.

Lemma Union_spec: forall A (v: A) P Q, Union _ P Q v <-> P v \/ Q v.
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  split; intros.
  + inversion H; auto.
  + destruct H; [apply Union_introl | apply Union_intror]; auto.
Qed.

Lemma Disjoint_spec: forall A P Q, Disjoint A P Q <-> (forall x, P x -> Q x -> False).
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros; split; intros.
  + inversion H.
    eapply H2.
    unfold In; rewrite Intersection_spec; split; eauto.
  + constructor.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
    intros.
    unfold In; rewrite Intersection_spec.
    intro; apply H with x; tauto.
Qed.

Lemma Singleton_spec: forall U x y, (Singleton U x) y <-> x = y.
Proof.
(* Goal: forall (U : Type) (x y : U), iff (In U (Singleton U x) y) (@eq U x y) *)
  intros; split; intro.
  + inversion H; auto.
  + subst; constructor.
Qed.

Lemma Included_Full_set: forall A P, Included A P (Full_set A).
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  hnf; unfold In; intros.
(* Goal: Full_set A x *)
  apply Full_set_spec; auto.
Qed.

Lemma Intersection_Complement: forall A (P Q: Ensemble A),
  Same_set A
  (Intersection A (Complement A P) (Complement A Q))
  (Complement A (Union A P Q)).
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: Same_set A (Intersection A (Complement A P) (Complement A Q)) (Complement A (Union A P Q)) *)
  unfold Same_set, Included, Complement, Ensembles.In.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  split; intros.
  + rewrite Union_spec.
(* Goal: and (@ex A (fun x : A => and (X x) (@eq B y (f x)))) (@ex A (fun x : A => and (Y x) (@eq B y (f x)))) *)
    rewrite Intersection_spec in H.
(* Goal: iff (and (x a) (x0 a)) (and (y a) (y0 a)) *)
    tauto.
  + rewrite Union_spec in H.
(* Goal: iff (Intersection U A B x) (B x) *)
    rewrite Intersection_spec.
(* Goal: iff (and (x a) (x0 a)) (and (y a) (y0 a)) *)
    tauto.
Qed.

Lemma Union_iff: forall U A B x, Ensembles.In U (Union U A B) x <-> Ensembles.In U A x \/ Ensembles.In U B x.
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros; split; intros.
  + apply Constructive_sets.Union_inv; auto.
  + destruct H; [apply Union_introl | apply Union_intror]; auto.
Qed.

Lemma Empty_set_iff: forall U x, Ensembles.In U (Empty_set U) x <-> False.
Proof.
  intros; split; intro; inversion H.
Qed.

Lemma Singleton_iff: forall U x y, Ensembles.In U (Singleton U x) y <-> x = y.
Proof.
(* Goal: forall (U : Type) (x y : U), iff (In U (Singleton U x) y) (@eq U x y) *)
  intros; split; intro.
  + inversion H; auto.
  + subst; constructor.
Qed.

Arguments Included {U} B C.
Arguments Same_set {U} B C.

Lemma Same_set_refl: forall A (S : Ensemble A), Same_set S S. Proof. intros; split; intro; tauto. Qed.

Lemma Same_set_sym: forall A (S1 S2 : Ensemble A), Same_set S1 S2 -> Same_set S2 S1. Proof. intros; destruct H; split; auto. Qed.

Lemma Same_set_trans: forall A (S1 S2 S3: Ensemble A), Same_set S1 S2 -> Same_set S2 S3 -> Same_set S1 S3.
Proof. intros; destruct H, H0; split; repeat intro; [apply H0, H, H3 | apply H1, H2, H3]. Qed.

Add Parametric Relation {A} : (Ensemble A) Same_set
    reflexivity proved by (Same_set_refl A)
    symmetry proved by (Same_set_sym A)
    transitivity proved by (Same_set_trans A) as Same_set_rel.

Lemma Same_set_spec: forall A P Q, Same_set P Q <-> (pointwise_relation A iff) P Q.
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: iff (@Same_set A P Q) (@pointwise_relation A Prop iff P Q) *)
  unfold Same_set, Included, In, pointwise_relation.
(* Goal: iff (@ex A (fun x0 : A => and (Empty_set A x0) (@eq B x (f x0)))) (Empty_set B x) *)
  firstorder.
Qed.

Lemma Complement_Empty_set: forall A, Same_set (Complement A (Empty_set _)) (Full_set _).
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  rewrite Same_set_spec.
(* Goal: @pointwise_relation A Prop iff (Complement A (Empty_set A)) (Full_set A) *)
  intro a.
(* Goal: iff (Complement V x a) (Complement V y a) *)
  unfold Complement, Ensembles.In.
(* Goal: iff (not (Empty_set A a)) (Full_set A a) *)
  pose proof Empty_set_iff _ a.
(* Goal: iff (not (Empty_set A a)) (Full_set A a) *)
  pose proof Full_set_spec _ a.
(* Goal: iff (and (x a) (x0 a)) (and (y a) (y0 a)) *)
  tauto.
Qed.

Lemma Intersection_comm: forall A P Q, Same_set (Intersection A P Q) (Intersection A Q P).
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  rewrite Same_set_spec; hnf; intros.
(* Goal: iff (Intersection B X Y (f x)) (Intersection A (fun x : A => X (f x)) (fun x : A => Y (f x)) x) *)
  rewrite !Intersection_spec.
(* Goal: iff (and (x a) (x0 a)) (and (y a) (y0 a)) *)
  tauto.
Qed.

Lemma Intersection_assoc: forall A P Q R, Same_set (Intersection A (Intersection A P Q) R) (Intersection A P (Intersection A Q R)).
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  rewrite Same_set_spec; hnf; intros.
(* Goal: iff (Intersection B X Y (f x)) (Intersection A (fun x : A => X (f x)) (fun x : A => Y (f x)) x) *)
  rewrite !Intersection_spec.
(* Goal: iff (and (x a) (x0 a)) (and (y a) (y0 a)) *)
  tauto.
Qed.

Lemma Union_comm: forall A P Q, Same_set (Union A P Q) (Union A Q P).
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  rewrite Same_set_spec; hnf; intros.
(* Goal: iff (Union B X Y (f x)) (Union A (fun x : A => X (f x)) (fun x : A => Y (f x)) x) *)
  rewrite !Union_spec.
(* Goal: iff (and (x a) (x0 a)) (and (y a) (y0 a)) *)
  tauto.
Qed.

Lemma Union_assoc: forall A P Q R, Same_set (Union A (Union A P Q) R) (Union A P (Union A Q R)).
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  rewrite Same_set_spec; hnf; intros.
(* Goal: iff (Union B X Y (f x)) (Union A (fun x : A => X (f x)) (fun x : A => Y (f x)) x) *)
  rewrite !Union_spec.
(* Goal: iff (and (x a) (x0 a)) (and (y a) (y0 a)) *)
  tauto.
Qed.

Lemma Intersection_Union_distr_l: forall A P Q R,
  Same_set (Intersection A (Union A Q R) P)
   (Union A (Intersection A Q P) (Intersection A R P)).
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: @Same_set U (Intersection U A B) B *)
  rewrite Same_set_spec; intro x.
(* Goal: iff (Intersection A P (Union A Q R) x) (Union A (Intersection A P Q) (Intersection A P R) x) *)
  rewrite !Intersection_spec, !Union_spec, !Intersection_spec.
(* Goal: iff (and (x a) (x0 a)) (and (y a) (y0 a)) *)
  tauto.
Qed.

Lemma Intersection_Union_distr_r: forall A P Q R,
  Same_set (Intersection A P (Union A Q R))
   (Union A (Intersection A P Q) (Intersection A P R)).
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: @Same_set U (Intersection U A B) B *)
  rewrite Same_set_spec; intro x.
(* Goal: iff (Intersection A P (Union A Q R) x) (Union A (Intersection A P Q) (Intersection A P R) x) *)
  rewrite !Intersection_spec, !Union_spec, !Intersection_spec.
(* Goal: iff (and (x a) (x0 a)) (and (y a) (y0 a)) *)
  tauto.
Qed.

Instance Included_proper (V: Type): Proper (Same_set ==> Same_set ==> iff) (@Included V).
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  hnf; intros.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  hnf; intros.
(* Goal: @Same_set B (@image_set A B x x0) (@image_set A B y y0) *)
  rewrite Same_set_spec in *.
(* Goal: iff (@Included V x x0) (@Included V y y0) *)
  unfold pointwise_relation, Included, Ensembles.In in *.
(* Goal: iff (@ex A (fun x0 : A => and (Empty_set A x0) (@eq B x (f x0)))) (Empty_set B x) *)
  firstorder.
Defined.

Instance complement_proper (V: Type): Proper (Same_set ==> Same_set) (Complement V).
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  hnf; intros.
(* Goal: @Same_set B (@image_set A B x x0) (@image_set A B y y0) *)
  rewrite Same_set_spec in *.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  hnf; intros.
(* Goal: iff (Complement V x a) (Complement V y a) *)
  unfold Complement, Ensembles.In.
(* Goal: iff (not (x a)) (not (y a)) *)
  specialize (H a).
(* Goal: iff (and (x a) (x0 a)) (and (y a) (y0 a)) *)
  tauto.
Defined.

Instance Union_proper (V: Type): Proper (Same_set ==> Same_set ==> Same_set) (Union V).
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  hnf; intros.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  hnf; intros.
(* Goal: @Same_set B (@image_set A B x x0) (@image_set A B y y0) *)
  rewrite Same_set_spec in *.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  unfold pointwise_relation in *; intros.
(* Goal: iff (Union B X Y (f x)) (Union A (fun x : A => X (f x)) (fun x : A => Y (f x)) x) *)
  rewrite !Union_spec.
(* Goal: iff (@ex A (fun x0 : A => and (Empty_set A x0) (@eq B x (f x0)))) (Empty_set B x) *)
  firstorder.
Defined.

Instance Disjoint_proper (V: Type): Proper (Same_set ==> Same_set ==> iff) (Disjoint V).
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  hnf; intros.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  hnf; intros.
(* Goal: @Same_set B (@image_set A B x x0) (@image_set A B y y0) *)
  rewrite Same_set_spec in *.
(* Goal: @pointwise_relation B Prop iff (@image_set A B x x0) (@image_set A B y y0) *)
  unfold pointwise_relation in *.
(* Goal: iff (Disjoint A P Q) (Disjoint A Q P) *)
  rewrite !Disjoint_spec.
(* Goal: iff (@ex A (fun x0 : A => and (Empty_set A x0) (@eq B x (f x0)))) (Empty_set B x) *)
  firstorder.
Defined.

Lemma Union_Included {A: Type}: forall P Q R, Included (Union A P Q) R <-> Included P R /\ Included Q R.
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: iff (@Included A (Union A P Q) R) (and (@Included A P R) (@Included A Q R)) *)
  unfold Included.
(* Goal: iff (forall (x : A) (_ : In A (Union A P Q) x), In A R x) (and (forall (x : A) (_ : In A P x), In A R x) (forall (x : A) (_ : In A Q x), In A R x)) *)
  pose proof Union_iff A P Q.
(* Goal: iff (@ex A (fun x0 : A => and (Empty_set A x0) (@eq B x (f x0)))) (Empty_set B x) *)
  firstorder.
Qed.

Lemma left_Included_Union {A: Type}: forall P Q, Included P (Union A P Q).
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: @Included A Q (Union A P Q) *)
  intros ? ?.
(* Goal: In A (Union A P Q) x *)
  rewrite Union_iff.
(* Goal: iff (and (x a) (x0 a)) (and (y a) (y0 a)) *)
  tauto.
Qed.

Lemma right_Included_Union {A: Type}: forall P Q, Included Q (Union A P Q).
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: @Included A Q (Union A P Q) *)
  intros ? ?.
(* Goal: In A (Union A P Q) x *)
  rewrite Union_iff.
(* Goal: iff (and (x a) (x0 a)) (and (y a) (y0 a)) *)
  tauto.
Qed.

Lemma Union_Empty_left {A: Type}: forall P, Same_set (Union _ (Empty_set A) P) P.
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  rewrite Same_set_spec.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  hnf; intros.
(* Goal: iff (Union A P (Empty_set A) a) (P a) *)
  rewrite Union_spec.
(* Goal: iff (or (P a) (Empty_set A a)) (P a) *)
  pose proof Noone_in_empty A a.
(* Goal: iff (and (x a) (x0 a)) (and (y a) (y0 a)) *)
  tauto.
Qed.

Lemma Union_Empty_right {A: Type}: forall P, Same_set (Union _ P (Empty_set A)) P.
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  rewrite Same_set_spec.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  hnf; intros.
(* Goal: iff (Union A P (Empty_set A) a) (P a) *)
  rewrite Union_spec.
(* Goal: iff (or (P a) (Empty_set A a)) (P a) *)
  pose proof Noone_in_empty A a.
(* Goal: iff (and (x a) (x0 a)) (and (y a) (y0 a)) *)
  tauto.
Qed.

Lemma Intersection_Full_left {A: Type}: forall P, Same_set (Intersection _ (Full_set A) P) P.
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  rewrite Same_set_spec.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  hnf; intros.
(* Goal: iff (Intersection U A B x) (B x) *)
  rewrite Intersection_spec.
(* Goal: iff (and (P a) (Full_set A a)) (P a) *)
  pose proof Full_set_spec A a.
(* Goal: iff (and (x a) (x0 a)) (and (y a) (y0 a)) *)
  tauto.
Qed.

Lemma Intersection_Full_right {A: Type}: forall P, Same_set (Intersection _ P (Full_set A)) P.
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  rewrite Same_set_spec.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  hnf; intros.
(* Goal: iff (Intersection U A B x) (B x) *)
  rewrite Intersection_spec.
(* Goal: iff (and (P a) (Full_set A a)) (P a) *)
  pose proof Full_set_spec A a.
(* Goal: iff (and (x a) (x0 a)) (and (y a) (y0 a)) *)
  tauto.
Qed.

Lemma Intersection_Empty_left {A: Type}: forall P, Same_set (Intersection _ (Empty_set A) P) (Empty_set A).
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  rewrite Same_set_spec.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  hnf; intros.
(* Goal: iff (Intersection U A B x) (B x) *)
  rewrite Intersection_spec.
(* Goal: iff (and (P a) (Empty_set A a)) (Empty_set A a) *)
  pose proof Empty_set_spec A a.
(* Goal: iff (and (x a) (x0 a)) (and (y a) (y0 a)) *)
  tauto.
Qed.

Lemma Intersection_Empty_right {A: Type}: forall P, Same_set (Intersection _ P (Empty_set A)) (Empty_set A).
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  rewrite Same_set_spec.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  hnf; intros.
(* Goal: iff (Intersection U A B x) (B x) *)
  rewrite Intersection_spec.
(* Goal: iff (and (P a) (Empty_set A a)) (Empty_set A a) *)
  pose proof Empty_set_spec A a.
(* Goal: iff (and (x a) (x0 a)) (and (y a) (y0 a)) *)
  tauto.
Qed.

Lemma Intersection_absort_right: forall U (A B: Ensemble U), Included A B -> Same_set (Intersection _ A B) A.
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: @Same_set U (Intersection U A B) B *)
  rewrite Same_set_spec; intro x.
(* Goal: iff (Intersection U A B x) (B x) *)
  rewrite Intersection_spec.
(* Goal: iff (and (A x) (B x)) (B x) *)
  specialize (H x); unfold Ensembles.In in H.
(* Goal: iff (and (x a) (x0 a)) (and (y a) (y0 a)) *)
  tauto.
Qed.

Lemma Intersection_absort_left: forall U (A B: Ensemble U), Included B A -> Same_set (Intersection _ A B) B.
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: @Same_set U (Intersection U A B) B *)
  rewrite Same_set_spec; intro x.
(* Goal: iff (Intersection U A B x) (B x) *)
  rewrite Intersection_spec.
(* Goal: iff (and (A x) (B x)) (B x) *)
  specialize (H x); unfold Ensembles.In in H.
(* Goal: iff (and (x a) (x0 a)) (and (y a) (y0 a)) *)
  tauto.
Qed.

Lemma Complement_Included_rev: forall (U: Type) P Q, Included P Q -> Included (Complement U Q) (Complement U P).
Proof.
(* Goal: forall (U : Type) (P Q : Ensemble U) (_ : @Included U P Q), @Included U (Complement U Q) (Complement U P) *)
  unfold Included, Complement, Ensembles.In.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: iff (@ex A (fun x0 : A => and (Empty_set A x0) (@eq B x (f x0)))) (Empty_set B x) *)
  firstorder.
Qed.

Instance Intersection_proper {A}: Proper (Same_set ==> Same_set ==> Same_set) (Intersection A).
Proof.
(* Goal: @Proper (forall (_ : Ensemble A) (_ : forall _ : A, B), Ensemble B) (@respectful (Ensemble A) (forall _ : forall _ : A, B, Ensemble B) (@Same_set A) (@respectful (forall _ : A, B) (Ensemble B) (@eq (forall _ : A, B)) (@Same_set B))) (@image_set A B) *)
  do 2 (hnf; intros).
(* Goal: @Same_set B (@image_set A B x x0) (@image_set A B y y0) *)
  rewrite Same_set_spec in *.
(* Goal: iff (not (x a)) (not (y a)) *)
  intro a; specialize (H0 a); specialize (H a).
(* Goal: iff (Intersection B X Y (f x)) (Intersection A (fun x : A => X (f x)) (fun x : A => Y (f x)) x) *)
  rewrite !Intersection_spec.
(* Goal: iff (and (x a) (x0 a)) (and (y a) (y0 a)) *)
  tauto.
Defined.

Lemma Included_Disjoint: forall A P Q P' Q',
  Included P P' ->
  Included Q Q' ->
  Disjoint A P' Q' ->
  Disjoint A P Q.
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: Disjoint A P Q *)
  rewrite Disjoint_spec in H1 |- *.
(* Goal: forall (x : A) (_ : P x) (_ : Q x), False *)
  intros; apply (H1 x).
  + apply H; auto.
  + apply H0; auto.
Qed.

Lemma Union_left_Disjoint: forall A P Q R,
  Disjoint A (Union A P Q) R <-> Disjoint A P R /\ Disjoint A Q R.
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: iff (Disjoint A P Q) (Disjoint A Q P) *)
  rewrite !Disjoint_spec.
(* Goal: iff (forall (x : A) (_ : R x) (_ : Union A P Q x), False) (and (forall (x : A) (_ : R x) (_ : P x), False) (forall (x : A) (_ : R x) (_ : Q x), False)) *)
  pose proof (fun x => Union_spec A x P Q).
(* Goal: iff (@ex A (fun x0 : A => and (Empty_set A x0) (@eq B x (f x0)))) (Empty_set B x) *)
  firstorder.
Qed.

Lemma Union_right_Disjoint: forall A P Q R,
  Disjoint A R (Union A P Q) <-> Disjoint A R P /\ Disjoint A R Q.
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: iff (Disjoint A P Q) (Disjoint A Q P) *)
  rewrite !Disjoint_spec.
(* Goal: iff (forall (x : A) (_ : R x) (_ : Union A P Q x), False) (and (forall (x : A) (_ : R x) (_ : P x), False) (forall (x : A) (_ : R x) (_ : Q x), False)) *)
  pose proof (fun x => Union_spec A x P Q).
(* Goal: iff (@ex A (fun x0 : A => and (Empty_set A x0) (@eq B x (f x0)))) (Empty_set B x) *)
  firstorder.
Qed.

Lemma Included_Complement_Disjoint: forall A P Q,
  (Included P (Complement _ Q)) <-> Disjoint A P Q.
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: iff (@Included A P (Complement A Q)) (Disjoint A P Q) *)
  unfold Included, Complement, In.
(* Goal: iff (forall (x : A) (_ : P x), not (Q x)) (Disjoint A P Q) *)
  rewrite Disjoint_spec.
(* Goal: iff (@ex A (fun x0 : A => and (Empty_set A x0) (@eq B x (f x0)))) (Empty_set B x) *)
  firstorder.
Qed.

Lemma Disjoint_comm: forall A P Q,
  Disjoint A P Q <-> Disjoint A Q P.
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: iff (Disjoint A P Q) (Disjoint A Q P) *)
  rewrite !Disjoint_spec.
(* Goal: iff (@ex A (fun x0 : A => and (Empty_set A x0) (@eq B x (f x0)))) (Empty_set B x) *)
  firstorder.
Qed.

Lemma Disjoint_Empty_set_right: forall {A} (P: Ensemble A), Disjoint A P (Empty_set A).
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: Disjoint A P (Empty_set A) *)
  rewrite Disjoint_comm.
(* Goal: Disjoint A (Empty_set A) P *)
  apply Included_Complement_Disjoint.
(* Goal: @Included A (Empty_set A) (Complement A P) *)
  apply Constructive_sets.Included_Empty.
Qed.

Lemma Disjoint_Empty_set_left: forall {A} (P: Ensemble A), Disjoint A (Empty_set A) P.
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: Disjoint A (Empty_set A) P *)
  apply Included_Complement_Disjoint.
(* Goal: @Included A (Empty_set A) (Complement A P) *)
  apply Constructive_sets.Included_Empty.
Qed.

Lemma Included_trans: forall {A} (P Q R: Ensemble A), Included P Q -> Included Q R -> Included P R.
Proof.
(* Goal: forall (A : Type) (P Q R : Ensemble A) (_ : @Included A Q R), @Included A (Intersection A P Q) R *)
  unfold Included, Ensembles.In.
(* Goal: iff (@ex A (fun x0 : A => and (Empty_set A x0) (@eq B x (f x0)))) (Empty_set B x) *)
  intros; firstorder.
Qed.

Lemma Intersection1_Included: forall {A} P Q R, Included P R -> Included (Intersection A P Q) R.
Proof.
(* Goal: forall (A : Type) (P Q R : Ensemble A) (_ : @Included A Q R), @Included A (Intersection A P Q) R *)
  unfold Included, Ensembles.In.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: R x *)
  rewrite Intersection_spec in H0.
(* Goal: iff (@ex A (fun x0 : A => and (Empty_set A x0) (@eq B x (f x0)))) (Empty_set B x) *)
  firstorder.
Qed.

Lemma Intersection2_Included: forall {A} P Q R, Included Q R -> Included (Intersection A P Q) R.
Proof.
(* Goal: forall (A : Type) (P Q R : Ensemble A) (_ : @Included A Q R), @Included A (Intersection A P Q) R *)
  unfold Included, Ensembles.In.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: R x *)
  rewrite Intersection_spec in H0.
(* Goal: iff (@ex A (fun x0 : A => and (Empty_set A x0) (@eq B x (f x0)))) (Empty_set B x) *)
  firstorder.
Qed.

Lemma Included_refl: forall A P, @Included A P P.
Proof.
(* Goal: forall (A : Type) (P : Ensemble A), @Included A P P *)
  intros; hnf; auto.
Qed.

Definition app_same_set {A: Type} {P Q: Ensemble A} (H: Same_set P Q) (x: A): P x <-> Q x := proj1 (Same_set_spec A P Q) H x.

Coercion app_same_set : Same_set >-> Funclass.

(* TODO: rename it into preimage set *)
Definition respectful_set {A B: Type} (X: Ensemble B) (f: A -> B): Ensemble A := fun x => X (f x).

Inductive image_set {A B: Type}: Ensemble A -> (A -> B) -> Ensemble B :=
  | image_set_intro: forall (X: Ensemble A) (f: A -> B) (x: A), X x -> image_set X f (f x).

Lemma image_set_spec: forall {A B: Type} f X (y: B),
  image_set X f y <-> exists x: A, X x /\ y = f x.
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  split; intros.
  + inversion H; subst.
(* Goal: @ex A (fun x0 : A => and (X x0) (@eq B (f x) (f x0))) *)
    exists x.
(* Goal: and (X x) (@eq B (f x) (f x)) *)
    split; auto.
  + destruct H as [x [?H ?H]].
(* Goal: @ex A (fun x1 : A => and (x x1) (@eq B a (x0 x1))) *)
    subst.
(* Goal: @image_set A B X f (f x) *)
    constructor; auto.
Qed.

Instance respectful_set_proper {A B: Type}: Proper (Same_set ==> pointwise_relation A (@eq B) ==> Same_set) respectful_set.
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: @Proper (forall (_ : Ensemble A) (_ : forall _ : A, B), Ensemble B) (@respectful (Ensemble A) (forall _ : forall _ : A, B, Ensemble B) (@Same_set A) (@respectful (forall _ : A, B) (Ensemble B) (@eq (forall _ : A, B)) (@Same_set B))) (@image_set A B) *)
  do 2 (hnf; intros).
(* Goal: @Same_set B (@image_set A B x x0) (@image_set A B y y0) *)
  rewrite Same_set_spec in *.
(* Goal: @pointwise_relation B Prop iff (@image_set A B x x0) (@image_set A B y y0) *)
  unfold pointwise_relation in *.
(* Goal: iff (@respectful_set A B (Union B X Y) f x) (Union A (@respectful_set A B X f) (@respectful_set A B Y f) x) *)
  unfold respectful_set.
(* Goal: iff (@ex A (fun x0 : A => and (Empty_set A x0) (@eq B x (f x0)))) (Empty_set B x) *)
  firstorder.
  + rewrite <- H, <- H0; firstorder.
  + rewrite H, H0; firstorder.
Qed.

Instance image_set_proper2 {A B: Type}: Proper (Same_set ==> eq ==> Same_set) (@image_set A B).
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: @Proper (forall (_ : Ensemble A) (_ : forall _ : A, B), Ensemble B) (@respectful (Ensemble A) (forall _ : forall _ : A, B, Ensemble B) (@Same_set A) (@respectful (forall _ : A, B) (Ensemble B) (@eq (forall _ : A, B)) (@Same_set B))) (@image_set A B) *)
  do 2 (hnf; intros).
(* Goal: @Same_set B (@image_set A B x x0) (@image_set A B y y0) *)
  rewrite Same_set_spec in *.
(* Goal: @pointwise_relation B Prop iff (@image_set A B x x0) (@image_set A B y y0) *)
  unfold pointwise_relation in *.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: forall _ : @image_set A B X f y, @image_set A B Y f y *)
  rewrite !image_set_spec.
(* Goal: iff (@ex A (fun x0 : A => and (Empty_set A x0) (@eq B x (f x0)))) (Empty_set B x) *)
  firstorder.
  + subst. firstorder.
  + subst. firstorder.
Qed.

Lemma resp_Included: forall {A B: Type} (X Y: Ensemble B) (f: A -> B),
  Included X Y ->
  Included (respectful_set X f) (respectful_set Y f).
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: @Included A (@respectful_set A B X f) (@respectful_set A B Y f) *)
  unfold respectful_set, Included, In.
(* Goal: @pointwise_relation B Prop iff (@image_set A B (@eq A a) f) (@eq B (f a)) *)
  intro x.
(* Goal: forall _ : X (f x), Y (f x) *)
  apply H.
Qed.

Lemma resp_Same_set: forall {A B: Type} (X Y: Ensemble B) (f: A -> B),
  Same_set X Y ->
  Same_set (respectful_set X f) (respectful_set Y f).
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: @Same_set B (@image_set A B X f) (@image_set A B Y f) *)
  unfold Same_set in *.
(* Goal: iff (and (x a) (x0 a)) (and (y a) (y0 a)) *)
  split; apply resp_Included; tauto.
Qed.

Lemma resp_Intersection: forall {A B: Type} (X Y: Ensemble B) (f: A -> B),
  Same_set
   (respectful_set (Intersection _ X Y) f)
   (Intersection _ (respectful_set X f) (respectful_set Y f)).
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: @Same_set A (@respectful_set A B (Complement B X) f) (Complement A (@respectful_set A B X f)) *)
  rewrite Same_set_spec; intros x.
(* Goal: iff (@respectful_set A B (Union B X Y) f x) (Union A (@respectful_set A B X f) (@respectful_set A B Y f) x) *)
  unfold respectful_set.
(* Goal: iff (Intersection B X Y (f x)) (Intersection A (fun x : A => X (f x)) (fun x : A => Y (f x)) x) *)
  rewrite !Intersection_spec.
(* Goal: iff (not (X (f x))) (not (X (f x))) *)
  reflexivity.
Qed.

Lemma resp_Union: forall {A B: Type} (X Y: Ensemble B) (f: A -> B) ,
  Same_set
   (respectful_set (Union _ X Y) f)
   (Union _ (respectful_set X f) (respectful_set Y f)).
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: @Same_set A (@respectful_set A B (Complement B X) f) (Complement A (@respectful_set A B X f)) *)
  rewrite Same_set_spec; intros x.
(* Goal: iff (@respectful_set A B (Union B X Y) f x) (Union A (@respectful_set A B X f) (@respectful_set A B Y f) x) *)
  unfold respectful_set.
(* Goal: iff (Union B X Y (f x)) (Union A (fun x : A => X (f x)) (fun x : A => Y (f x)) x) *)
  rewrite !Union_spec.
(* Goal: iff (not (X (f x))) (not (X (f x))) *)
  reflexivity.
Qed.

Lemma resp_Complement: forall {A B: Type} (X: Ensemble B) (f: A -> B),
  Same_set
   (respectful_set (Complement _ X) f)
   (Complement _ (respectful_set X f)).
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: @Same_set A (@respectful_set A B (Complement B X) f) (Complement A (@respectful_set A B X f)) *)
  rewrite Same_set_spec; intros x.
(* Goal: iff (@respectful_set A B (Complement B X) f x) (Complement A (@respectful_set A B X f) x) *)
  unfold respectful_set, Complement, In.
(* Goal: iff (not (X (f x))) (not (X (f x))) *)
  reflexivity.
Qed.

Lemma resp_Disjoint: forall {A B: Type} (X Y: Ensemble B) (f: A -> B),
  Disjoint _ X Y ->
  Disjoint _ (respectful_set X f) (respectful_set Y f).
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: Disjoint A (@respectful_set A B X f) (@respectful_set A B Y f) *)
  rewrite <- Included_Complement_Disjoint in *.
(* Goal: @Included A (@respectful_set A B X f) (Complement A (@respectful_set A B Y f)) *)
  rewrite <- resp_Complement.
(* Goal: @Included A (@respectful_set A B X f) (@respectful_set A B (Complement B Y) f) *)
  apply resp_Included; auto.
Qed.

Lemma resp_Empty: forall {A B: Type} (f: A -> B),
  Same_set (respectful_set (Empty_set _) f) (Empty_set _).
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  rewrite Same_set_spec.
(* Goal: @pointwise_relation B Prop iff (@image_set A B (@eq A a) f) (@eq B (f a)) *)
  intro x.
(* Goal: iff (@ex A (fun x0 : A => and (Empty_set A x0) (@eq B x (f x0)))) (Empty_set B x) *)
  pose proof Noone_in_empty A.
(* Goal: iff (@ex A (fun x0 : A => and (Empty_set A x0) (@eq B x (f x0)))) (Empty_set B x) *)
  pose proof Noone_in_empty B.
(* Goal: iff (@ex A (fun x0 : A => and (Empty_set A x0) (@eq B x (f x0)))) (Empty_set B x) *)
  firstorder.
Qed.

Lemma image_Included: forall {A B: Type} (f: A -> B) (X Y: Ensemble A),
  Included X Y ->
  Included (image_set X f) (image_set Y f).
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: @Included B (@image_set A B X f) (@image_set A B Y f) *)
  unfold Included, In.
(* Goal: forall (x : B) (_ : @image_set A B X f x), @image_set A B Y f x *)
  intro y.
(* Goal: forall _ : @image_set A B X f y, @image_set A B Y f y *)
  rewrite !image_set_spec.
(* Goal: forall _ : @ex A (fun x : A => and (Intersection A X Y x) (@eq B y (f x))), and (@ex A (fun x : A => and (X x) (@eq B y (f x)))) (@ex A (fun x : A => and (Y x) (@eq B y (f x)))) *)
  intros [x [? ?]].
(* Goal: and (X x) (@eq B (f x) (f x)) *)
  exists x; split; auto.
(* Goal: Y x *)
  apply H; auto.
Qed.

Lemma image_Same_set: forall {A B: Type} (f: A -> B) (X Y: Ensemble A),
  Same_set X Y ->
  Same_set (image_set X f) (image_set Y f).
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: @Same_set B (@image_set A B X f) (@image_set A B Y f) *)
  unfold Same_set in *.
(* Goal: iff (and (x a) (x0 a)) (and (y a) (y0 a)) *)
  split; apply image_Included; tauto.
Qed.

Lemma image_Intersection: forall {A B: Type} (X Y: Ensemble A) (f: A -> B),
  Included
   (image_set (Intersection _ X Y) f)
   (Intersection _ (image_set X f) (image_set Y f)).
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: @Included B (@image_set A B (Intersection A X Y) f) (Intersection B (@image_set A B X f) (@image_set A B Y f)) *)
  unfold Included, In; intros y.
(* Goal: forall _ : @image_set A B (Intersection A X Y) f y, Intersection B (@image_set A B X f) (@image_set A B Y f) y *)
  rewrite !Intersection_spec, !image_set_spec.
(* Goal: forall _ : @ex A (fun x : A => and (Intersection A X Y x) (@eq B y (f x))), and (@ex A (fun x : A => and (X x) (@eq B y (f x)))) (@ex A (fun x : A => and (Y x) (@eq B y (f x)))) *)
  intros [x [? ?]].
(* Goal: and (@ex A (fun x : A => and (X x) (@eq B y (f x)))) (@ex A (fun x : A => and (Y x) (@eq B y (f x)))) *)
  rewrite Intersection_spec in H.
(* Goal: iff (and (x a) (x0 a)) (and (y a) (y0 a)) *)
  split; exists x; tauto.
Qed.

Lemma image_Union: forall {A B: Type} (X Y: Ensemble A) (f: A -> B),
  Same_set
   (image_set (Union _ X Y) f)
   (Union _ (image_set X f) (image_set Y f)).
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: @Same_set B (@image_set A B (Union A X Y) f) (Union B (@image_set A B X f) (@image_set A B Y f)) *)
  rewrite Same_set_spec; intros y.
(* Goal: iff (@image_set A B (Union A X Y) f y) (Union B (@image_set A B X f) (@image_set A B Y f) y) *)
  rewrite !Union_spec, !image_set_spec.
(* Goal: iff (@ex A (fun x : A => and (Union A X Y x) (@eq B y (f x)))) (or (@ex A (fun x : A => and (X x) (@eq B y (f x)))) (@ex A (fun x : A => and (Y x) (@eq B y (f x))))) *)
  pose proof (fun x => Union_spec A x X Y).
(* Goal: iff (@ex A (fun x0 : A => and (Empty_set A x0) (@eq B x (f x0)))) (Empty_set B x) *)
  firstorder.
Qed.

Lemma image_Disjoint_rev: forall {A B: Type} (X Y: Ensemble A) (f: A -> B),
  Disjoint _ (image_set X f) (image_set Y f) ->
  Disjoint _ X Y.
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: Disjoint A X Y *)
  rewrite Disjoint_spec in *.
(* Goal: forall (x : A) (_ : X x) (_ : Y x), False *)
  intros x ? ?.
(* Goal: @image_set A B X f (f x) *)
  apply (H (f x)); constructor; auto.
Qed.

Lemma image_Empty: forall {A B: Type} (f: A -> B),
  Same_set (image_set (Empty_set _) f) (Empty_set _).
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  rewrite Same_set_spec.
(* Goal: @pointwise_relation B Prop iff (@image_set A B (@eq A a) f) (@eq B (f a)) *)
  intro x.
(* Goal: iff (@image_set A B (@eq A a) f x) (@eq B (f a) x) *)
  rewrite image_set_spec.
(* Goal: iff (@ex A (fun x0 : A => and (Empty_set A x0) (@eq B x (f x0)))) (Empty_set B x) *)
  pose proof Noone_in_empty A.
(* Goal: iff (@ex A (fun x0 : A => and (Empty_set A x0) (@eq B x (f x0)))) (Empty_set B x) *)
  pose proof Noone_in_empty B.
(* Goal: iff (@ex A (fun x0 : A => and (Empty_set A x0) (@eq B x (f x0)))) (Empty_set B x) *)
  firstorder.
Qed.

Lemma image_single: forall {A B: Type} (a: A) (f: A -> B),
  Same_set (image_set (eq a) f) (eq (f a)).
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  rewrite Same_set_spec.
(* Goal: @pointwise_relation B Prop iff (@image_set A B (@eq A a) f) (@eq B (f a)) *)
  intro x.
(* Goal: iff (@image_set A B (@eq A a) f x) (@eq B (f a) x) *)
  rewrite image_set_spec.
(* Goal: iff (@ex A (fun x0 : A => and (@eq A a x0) (@eq B x (f x0)))) (@eq B (f a) x) *)
  split; intros; eauto.
(* Goal: @eq B (f a) x *)
  destruct H as [? [? ?]]; subst; auto.
Qed.

Definition Countable_Union (A: Type) (P: nat -> Ensemble A) : Ensemble A :=
  fun x => exists i, P i x.

Definition Non_Empty {U: Type} (A: Ensemble U): Prop := exists x, A x.

Definition Binart_set_list (U: Type) (A B: Ensemble U): nat -> Ensemble U :=
  fun n => match n with | 0 => A | 1 => B | _ => Empty_set _ end.

Lemma Union_is_Countable_Union: forall {U: Type} (A B: Ensemble U),
  Same_set (Union _ A B) (Countable_Union _ (Binart_set_list _ A B)).
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  rewrite Same_set_spec.
(* Goal: @pointwise_relation U Prop iff (Union U A B) (Countable_Union U (Binart_set_list U A B)) *)
  intros x.
(* Goal: iff (Union U A B x) (Countable_Union U (Binart_set_list U A B) x) *)
  rewrite Union_spec; unfold Countable_Union.
(* Goal: iff (or (A x) (B x)) (@ex nat (fun i : nat => Binart_set_list U A B i x)) *)
  split.
  + intros [? | ?].
    - exists 0; auto.
    - exists 1; auto.
  + intros [[ | [ | ]] ?].
    - left; auto.
    - right; auto.
    - intros; inversion H.
Qed.

Lemma Intersection_is_Complement_Union (classic: forall P: Prop, P \/ ~ P): forall {U: Type} (A B: Ensemble U),
  Same_set (Intersection _ A B) (Complement _ (Union _ (Complement _ A) (Complement _ B))).
Proof.
(* Goal: forall (U : Type) (A B : Ensemble U), @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  intros.
(* Goal: @Same_set U (Intersection U A B) (Complement U (Union U (Complement U A) (Complement U B))) *)
  rewrite Same_set_spec.
(* Goal: iff (Complement V x a) (Complement V y a) *)
  intros x; unfold Complement, Ensembles.In.
(* Goal: iff (Intersection U A B x) (not (Union U (fun x : U => not (A x)) (fun x : U => not (B x)) x)) *)
  rewrite Union_spec, Intersection_spec.
(* Goal: iff (and (x a) (x0 a)) (and (y a) (y0 a)) *)
  destruct (classic (A x)), (classic (B x)); tauto.
Qed.

Arguments Included: clear implicits.
Arguments Same_set: clear implicits.
