Set Implicit Arguments.
Set Contextual Implicit.

Require Import Utf8.
Require Import Setoid.
Require Import Morphisms.
Require Import Relation_Definitions.

Definition Ens `{X:Set}:= X → Prop.

Definition subset `{X:Set} (A B:@Ens X):= ∀ x, A x → B x.
Definition emptyset `{X:Set}:= (λ x:X, False).
Definition same_set `{X:Set} (A B:@Ens X):= (∀ (x:X), A x ↔ B x).
Infix "≅":= (same_set) (at level 75).

Lemma same_set_refl `{X:Set}: ∀ A:(@Ens X), A ≅ A.
Proof.
  intros A;split;intro H;assumption.
Qed.

Lemma same_set_sym `{X:Set}:
  ∀ A B:(@Ens X), A ≅ B → B ≅ A.
Proof.
  intros A B Heq;
  split;intro Hx;
  [destruct (Heq x) as [_ H] | destruct (Heq x) as [H _]];
  apply (H Hx).
Qed.

Lemma same_set_trans `{X:Set}:
  ∀ A B C:(@Ens X), A ≅ B → B ≅ C → A ≅ C.
Proof.
  intros A B C HABeq HBCeq;split;intro Hx;
  [destruct (HABeq x) as [HAB _] | destruct (HABeq x) as [_ HAB]];
  [destruct (HBCeq x) as [HBC _] | destruct (HBCeq x) as [_ HBC]].
  apply (HBC (HAB Hx)).
  apply (HAB (HBC Hx)).
Qed.

Instance same_set_Equiv `{X:Set}: Equivalence (@same_set X).
Proof.
  split.
  - intro A.
    apply same_set_refl.
  - intros A B HAB.
    apply (same_set_sym HAB).
  - intros A B C HAB HBC.
    apply (same_set_trans HAB HBC).
Qed.