Require Import Compare_dec.
Require Import Coq.Init.Nat.
Require Import Setoid.
Require Import Coq.Lists.List.
Import ListNotations.
Require Import Coq.Program.Program.
Arguments id {_} _ /.
Arguments const {_ _} _ _ /.
Arguments compose {_ _ _} _ _ _ /.
Require Import Coq.Logic.Classical.

Unset Printing Records.

Axiom PE : forall P Q, P <-> Q -> P = Q.

Lemma proof_irrelevance (P : Prop) (H H' : P) :
  H = H'.
Proof.
  assert (P = True) as ->.
  - apply PE. tauto.
  - destruct H, H'. reflexivity.
Qed.

Class Functional {A : Type} (R : relation A) :=
  functionality : forall {x y y'}, R x y -> R x y' -> y = y'.

Fixpoint Any {A} (l : list A) (P : A -> Prop) :=
  match l with
  | [] => False
  | head :: tail => P head \/ Any tail P
  end.

Fixpoint All {A} (l : list A) (P : A -> Prop) :=
  match l with
  | [] => True
  | head :: tail => P head /\ All tail P
  end.

Parameter Set_ : Type.
Notation S := Set_.
Parameter In_Set : S -> S -> Prop.

Record Class :=
  build_class {
      element_predicate : S -> Prop
    }.

Class In_Class (x : S) (A : Class) :=
  in_class : A.(element_predicate) x.

Arguments In_Class : simpl never.

Notation "x ∈ A" := (In_Class x A) (at level 70).
Notation "x ∉ A" := (~ x ∈ A) (at level 70).

Definition class_of_all_sets : Class :=
  build_class (const True).

Instance in_class_of_all_sets (x : S) : x ∈ class_of_all_sets.
Proof. exact I. Qed.

Coercion set_to_class (x : S) : Class :=
  build_class (fun y => In_Set y x).

Record Element_Of (A : Class) :=
  build_element {
      element_value :> S;
      element_property : element_value ∈ A
    }.
Arguments build_element {_} _ _.
Arguments element_value {_} _.
Coercion Element_Of : Class >-> Sortclass.
Existing Instance element_property.

(* (** I don't know how to declar build_element as canonical structure, so I redefine it. *) *)
(* Canonical Structure build_element' {A : Class} (x : S) (H : x ∈ A) : *)
(*   Element_Of A := *)
(*   build_element x H. *)

Notation element x := (build_element x _).

Lemma element_equality {A : Class} {x y : A} :
  x = y :> S <-> x = y.
Proof.
  split.
  - destruct x as [x x_in_A], y as [y y_in_A]; cbn.
    intros ->. f_equal. apply proof_irrelevance.
  - intros ->. reflexivity.
Qed.

Instance element_stays_element {A B} x :
  x ∈ A ->
  forall x_in_B : x ∈ B,
    build_element x x_in_B ∈ A.
Proof. intros. exact _. Qed.

Lemma strip_element {A : Class} (x : A) {H : x ∈ A} :
  build_element x H = x.
Proof.
  apply element_equality. reflexivity.
Qed.

Definition Is_Subclass_Of (A B : Class) :=
  forall x, x ∈ A -> x ∈ B.

Notation "A ⊆ B" := (Is_Subclass_Of A B) (at level 70).
Notation "A ⊈ B" := (~ A ⊆ B) (at level 70).
Hint Unfold Is_Subclass_Of : core.

Instance subset_relation_reflexivity :
  Reflexive Is_Subclass_Of.
Proof. intros A x. exact id. Qed.

Instance subset_relation_transitivity :
  Transitive Is_Subclass_Of.
Proof. intros A B C AB BC x x_in_A. exact (BC x (AB x x_in_A)). Qed.

Add Relation S Is_Subclass_Of
    reflexivity proved by subset_relation_reflexivity
    transitivity proved by subset_relation_transitivity
      as subset_relation_is_preorder.

Add Parametric Morphism (x : S) : (In_Class x)
    with signature Is_Subclass_Of ==> impl
      as element_relation_subset_mor.
Proof. intros A B AB x_in_A. apply AB. exact x_in_A. Qed.

Axiom extensionality :
  forall A B : S,
    A = B <-> (forall x, x ∈ A <-> x ∈ B).

Ltac simplify :=
  repeat (cbn in * ||
          unshelve autorewrite with core sets in *; try exact _).

Ltac automation :=
  repeat (
      match goal with | [ x : Element_Of ?A |- _ ] => destruct x end ||
      eassumption ||
      simplify ||
      intuition || destruct_conjs || subst ||
      eauto with core sets ||
      match goal with
      | [ |- ex (const _) ] => simple refine (ex_intro _ _ _)
      | [ |- exists _, _ ] => eexists
      end ||
      autounfold).

Parameter empty_set : S.
Notation "∅" := empty_set.
Axiom in_empty_set_iff : forall x, x ∈ ∅ <-> False.
Hint Rewrite in_empty_set_iff : sets.

Lemma empty_set_ind (P : Prop) (x : ∅) : P.
Proof. exfalso. rewrite <- (in_empty_set_iff x). exact _. Qed.

Parameter big_union : S -> S.
Axiom in_big_union_iff :
  forall x A,
    x ∈ big_union A <-> (exists B : A, x ∈ B).
Hint Rewrite in_big_union_iff : sets.

Parameter power_set : S -> S.
Notation "'𝒫'" := power_set.

Axiom in_power_set_iff : forall A B, A ∈ 𝒫 B <-> A ⊆ B.
Hint Rewrite in_power_set_iff : sets.

Instance set_in_power_set (x : S) :
  x ∈ 𝒫 x.
Proof. automation. Qed.

Instance in_set_if_in_subset {A : S} (A' : 𝒫 A) (x : A') :
  x ∈ A.
Proof.
  assert (H : A' ∈ 𝒫 A) by exact _. rewrite in_power_set_iff in H.
  apply H. exact _.
Qed.

Lemma subset_extensionality {A} (A1 A2 : 𝒫 A) :
  (forall a : A, a ∈ A1 <-> a ∈ A2) ->
  A1 = A2.
Proof.
  intros H.
  apply element_equality. apply extensionality; intros a; split.
  - intros ?. apply (H (element (element a : A1) : A)). exact _.
  - intros ?. apply (H (element (element a : A2) : A)). exact _.
Qed.

Parameter replacement :
  forall R : relation S, Functional R -> S -> S.
Axiom in_replacement_iff :
  forall R `{Functional _ R} A y,
    y ∈ replacement R _ A <-> (exists x : A, R x y).
Hint Rewrite in_replacement_iff : sets.

Program Definition fun_replacement (A : S) (f : A -> S) : S :=
  replacement (fun x y => exists (H : x ∈ A), y = f (element x)) _ A.
Next Obligation.
  intros x y y'.
  intros [x_in_A ->] [x_in_A' ->].
  f_equal. apply element_equality; simplify. reflexivity.
Qed.
Notation "`{ y | x 'in' A }" := (fun_replacement A (fun x => y))
                                 (at level 0, y at level 99).
Lemma in_fun_replacement_iff A f y :
  y ∈ fun_replacement A f <-> exists x : A, y = f x.
Proof.
  unfold fun_replacement; simplify.
  split.
  - automation.
  - intros [x ->].
    exists x, _. destruct x.
    reflexivity.
Qed.
Global Opaque fun_replacement.
Hint Rewrite in_fun_replacement_iff : sets.

Instance fun_replacement_in_power_set (A B : S) (f : A -> B) :
  `{ f a | a in A } ∈ 𝒫 B.
Proof. automation. Qed.

Program Definition image_under {A B : S} (f : A -> B) (A' : 𝒫 A) :
  𝒫 B :=
  element `{ f (element a) | a in A' }.
Arguments image_under : simpl never.
Notation "f '' A" := (image_under f A) (at level 35, right associativity).

Lemma in_image_iff {A B : S} (f : A -> B) (A' : 𝒫 A) (y : B) :
  y ∈ f '' A' <-> exists x : A, x ∈ A' /\ y = f x.
Proof.
  unfold image_under; cbn. rewrite in_fun_replacement_iff.
  split.
  - intros [x ->%element_equality]. automation.
  - intros (x & ? & ->).
    exists (element x). cbn. rewrite strip_element. reflexivity.
Qed.
Hint Rewrite @in_image_iff : sets.

Instance in_image_under {A B : S} (A' : 𝒫 A) (f : A -> B) (x : A') :
  f (element x) ∈ f '' A'.
Proof. automation. Qed.

Lemma image_of_image {A B C : S} (f : A -> B) (g : B -> C) (A' : 𝒫 A) :
  g '' f '' A' = (g ∘ f) '' A'.
Proof.
  apply subset_extensionality; intros c.
  repeat setoid_rewrite in_image_iff; cbn.
  firstorder congruence.
Qed.

Lemma image_under_id {A} (A' : 𝒫 A) :
  id '' A' = A'.
Proof.
  apply subset_extensionality; intros a.
  rewrite in_image_iff; cbn.
  firstorder congruence.
Qed.

Program Definition image_of {A B : S} (f : A -> B) : 𝒫 B :=
  element `{ f a | a in A }.

Instance in_image_of {A B : S} (f : A -> B) (a : A) :
  f a ∈ image_of f.
Proof. unfold image_of. automation. Qed.

Program Definition conditional_fun_replacement
        (A : S) (P : A -> Prop) (f : forall x : A, P x -> S) :=
  replacement
    (fun x y => exists (H : x ∈ A) (P_x : P (element x)), y = f (element x) P_x) _ A.
Next Obligation.
  unfold Functional.
  intros x y1 y2.
  intros [x1_in_A [P_x1 ->]].
  intros [x2_in_A [P_x2 ->]].
  assert (x1_in_A = x2_in_A) as <- by apply proof_irrelevance.
  assert (P_x1 = P_x2) as <- by apply proof_irrelevance.
  reflexivity.
Qed.
Notation "`{ y | x 'in' A , P }" :=
  (conditional_fun_replacement A (fun x => P % type) (fun x (_ : P) => y))
    (at level 0, y at level 99).

Lemma in_conditional_fun_replacement_iff
      (A : S) (P : A -> Prop) (f : forall x : A, P x -> S) y :
  y ∈ conditional_fun_replacement A P f <->
  exists x : A, exists P_x : P x, y = f x P_x.
Proof.
  unfold conditional_fun_replacement. rewrite in_replacement_iff.
  change ((exists (x : A) (x_in_A : x ∈ A),
              (fun x' => exists P_x, y = f x' P_x) (build_element x x_in_A)) <->
          (exists (x : A) (P_x : P x), y = f x P_x)).
  setoid_rewrite strip_element.
  automation.
Qed.
Global Opaque conditional_fun_replacement.
Hint Rewrite in_conditional_fun_replacement_iff : sets.

Program Definition comprehension (A : S) (P : forall x : A, Prop) : 𝒫 A :=
  element (replacement (fun x y => x = y /\ exists (H : x ∈ A), P (element x)) _ A).
Next Obligation. unfold Functional. automation. Qed.
Next Obligation. automation. Qed.
Notation "`{ x 'in' A | P }" := (comprehension A (fun x => P))
                                 (at level 0, x at level 99).

Lemma in_comprehension_iff A P x :
  x ∈ comprehension A P <-> exists (H : x ∈ A), P (element x).
Proof.
  unfold comprehension; simplify.
  split.
  - intros (x' & <- & ? & H).
    exists _. exact H.
  - intros (? & H).
    exists (element x). split.
    + reflexivity.
    + exists _. exact H.
Defined.
Global Opaque comprehension.

Lemma in_comprehension_iff_typed (A : S) P (x : A) :
  x ∈ comprehension A P <-> P x.
Proof.
  rewrite in_comprehension_iff. setoid_rewrite strip_element. automation.
Qed.
Hint Rewrite in_comprehension_iff_typed : sets.

Lemma comprehension_condition {A : S} {P : A -> Prop} (x : `{ a in A | P a }) :
  P (element x).
Proof.
  assert (H : (element x : A) ∈ `{ a in A | P a }) by exact _.
  rewrite in_comprehension_iff_typed in H. exact H.
Qed.

Inductive Is_Accessible_By {A} (R : relation A) x : Prop :=
  is_accessible_intro : (forall y, R y x -> Is_Accessible_By R y) ->
                        Is_Accessible_By R x.
Definition Is_Terminating {A} (R : relation A) :=
  forall x, Is_Accessible_By R x.
Existing Class Is_Terminating.
Definition foundation {A} (R : relation A) {H : Is_Terminating R} :=
  H.

Lemma well_founded_induction
      {A : Type} (R : relation A) (P : A -> Prop) `{wf : Is_Terminating A R} :
  (forall a, (forall a', R a' a -> P a') -> P a) ->
  forall a, P a.
Proof.
  intros step a. specialize (wf a). induction wf as [a _ IH].
  apply step. exact IH.
Qed.

Axiom sets_are_well_founded : Is_Terminating In_Set.
Existing Instance sets_are_well_founded.

Lemma no_set_contains_itself (x : S) :
  x ∉ x.
Proof.
  intros x_in_x.
  induction (sets_are_well_founded x) as [x _ IH].
  apply (IH x).
  - exact x_in_x.
  - exact x_in_x.
Qed.

Lemma no_set_equals_its_power_set (x : S) :
  x <> 𝒫 x.
Proof.
  intros x_eq_power_set.
  enough (x ∈ x) by apply (no_set_contains_itself x _).
  rewrite x_eq_power_set at 2.
  apply set_in_power_set.
Qed.

Local Program Definition provisional_unordered_pair x y :=
  replacement (fun a b => (a = ∅ /\ b = x) \/ (a = 𝒫 ∅ /\ b = y))
              _
              (𝒫 (𝒫 ∅)).
Next Obligation.
  assert (∅ <> 𝒫 ∅) by apply no_set_equals_its_power_set.
  unfold Functional.
  automation.
Qed.

Local Lemma in_provisional_unordered_pair_iff x y z :
  z ∈ provisional_unordered_pair x y <-> (z = x) \/ (z = y).
Proof.
  unfold provisional_unordered_pair.
  rewrite in_replacement_iff. split.
  - automation.
  - intros [-> | ->].
    + simple refine (ex_intro _ (element ∅) _); automation.
    + simple refine (ex_intro _ (element (𝒫 ∅)) _); automation.
Qed.
Global Opaque provisional_unordered_pair.
Hint Rewrite in_provisional_unordered_pair_iff : sets.

Local Definition provisional_singleton x :=
  provisional_unordered_pair x x.

Local Lemma in_provisional_singleton x y :
  x ∈ provisional_singleton y <-> x = y.
Proof. unfold provisional_singleton. automation. Qed.
Global Opaque provisional_singleton.
Hint Rewrite in_provisional_singleton : sets.

Definition union (x y : S) :=
  big_union (provisional_unordered_pair x y).

Notation "x ∪ y" := (union x y) (at level 50).

Lemma in_union_iff x y z :
  x ∈ y ∪ z <-> x ∈ y \/ x ∈ z.
Proof.
  unfold union.
  split.
  - rewrite in_big_union_iff.
    intros [[B B_in_replacement] x_in_B].
    automation.
  - rewrite in_big_union_iff.
    intros [x_in_y | x_in_z].
    + simple refine (ex_intro _ (element y) _); automation.
    + simple refine (ex_intro _ (element z) _); automation.
Qed.
Global Opaque union.
Hint Rewrite in_union_iff : sets.

Instance in_union_intro1 x (A B : S) :
  x ∈ A ->
  x ∈ A ∪ B.
Proof. automation. Qed.

Instance in_union_intro2 x (A B : S) :
  x ∈ B ->
  x ∈ A ∪ B.
Proof. automation. Qed.

Instance in_union_intro_left (A B : S) x :
  x ∈ A ->
  x ∈ A ∪ B.
Proof. automation. Qed.

Instance in_union_intro_right (A B : S) x :
  x ∈ B ->
  x ∈ A ∪ B.
Proof. automation. Qed.

Definition adjunction x y :=
  provisional_singleton x ∪ y.
Notation "x @ y" := (adjunction x y) (at level 30). (* Same level as ^ *)

Lemma in_adjunction_iff x y z :
  x ∈ y @ z <-> x = y \/ x ∈ z.
Proof. unfold adjunction. automation. Qed.
Global Opaque adjunction.
Hint Rewrite in_adjunction_iff : sets.

Instance head_is_element_of_adjunction x y :
  x ∈ x @ y.
Proof. automation. Qed.
Hint Resolve head_is_element_of_adjunction : core.

Instance element_of_tail_is_element_of_adjunction (x y z : S) :
  x ∈ z -> x ∈ y @ z.
Proof. automation. Qed.
Hint Resolve element_of_tail_is_element_of_adjunction : core.

Fixpoint explicit_set (elements : list S) :=
  match elements with
  | [] => ∅
  | head :: tail => head @ explicit_set tail
  end.
Notation "`{ }" := (explicit_set []) (format "`{ }").

Notation "`{ x , .. , y }" := (explicit_set (cons x (.. (cons y nil) ..)))
                               (at level 0, x at level 99).

Lemma forall_elements_of_explicit_set_iff elements (P : S -> Prop) :
  (forall x : explicit_set elements, P x)
  <->
  All elements P.
Proof.
  transitivity (forall x, x ∈ explicit_set elements -> P x). {
    split.
    - intros H x Hx. exact (H (element x)).
    - automation.
  }
  induction elements; cbn.
  - automation.
  - setoid_rewrite in_adjunction_iff.
    automation.
Qed.

Lemma exists_element_of_explicit_set_iff elements (P : S -> Prop) :
  (exists x : explicit_set elements, P x)
  <->
  Any elements P.
Proof.
  transitivity (exists x, x ∈ explicit_set elements /\ P x). {
    split.
    - automation.
    - intros (x & Hx & P_x). exists (element x). exact P_x.
  }

  induction elements; cbn.
  - automation.
  - automation.
Qed.

Lemma in_explicit_set_iff elements x :
  x ∈ explicit_set elements <->
  Any elements (fun y => x = y).
Proof.
  rewrite <- exists_element_of_explicit_set_iff. split.
  - intros Hx. exists (element x). reflexivity.
  - automation.
Qed.

Lemma explicit_set_is_subset_of_explicit_set_iff elements1 elements2 :
  explicit_set elements1 ⊆ explicit_set elements2
  <->
  All elements1 (fun x => Any elements2 (fun y => x = y)).
Proof.
  unfold Is_Subclass_Of.
  rewrite <- forall_elements_of_explicit_set_iff.
  split.
  - intros. rewrite <- in_explicit_set_iff. automation.
  - intros. rewrite in_explicit_set_iff. exact (H (element x)).
Qed.

Lemma explicit_set_equals_explicit_set_iff elements1 elements2 :
  explicit_set elements1 = explicit_set elements2
  <->
  All elements1 (fun x => Any elements2 (fun y => x = y)) /\
  All elements2 (fun x => Any elements1 (fun y => x = y)).
Proof.
  rewrite extensionality.
  transitivity (explicit_set elements1 ⊆ explicit_set elements2 /\
                explicit_set elements2 ⊆ explicit_set elements1). {
    firstorder.
  }
  setoid_rewrite explicit_set_is_subset_of_explicit_set_iff.
  reflexivity.
Qed.

Global Opaque explicit_set.
Arguments explicit_set : simpl never.
Hint Rewrite forall_elements_of_explicit_set_iff : sets.
Hint Rewrite exists_element_of_explicit_set_iff : sets.
Hint Rewrite in_explicit_set_iff : sets.
Hint Rewrite explicit_set_is_subset_of_explicit_set_iff : sets.
Hint Rewrite explicit_set_equals_explicit_set_iff : sets.

Lemma unordered_pair_equals_unordered_pair_iff x y u v :
  `{x, y} = `{u, v} <-> (x = u /\ y = v) \/ (x = v /\ u = y).
Proof. automation. Qed.
Hint Rewrite unordered_pair_equals_unordered_pair_iff : sets.

Definition indexed_union (A : S) (f : A -> S) :=
  big_union `{ f x | x in A }.

Notation "⋃ x ∈ A , y" := (indexed_union A (fun x => y))
                            (at level 65, x ident, right associativity).
Lemma in_indexed_union_iff (A : S) (f : A -> S) (z : S) :
  z ∈ ⋃ x ∈ A, f x <-> exists x : A, z ∈ f x.
Proof.
  unfold indexed_union.
  rewrite in_big_union_iff.
  transitivity (exists B, B ∈ `{ f x | x in A } /\ z ∈ B). {
    split.
    - intros (B & H). exists B. split; exact _.
    - intros (B & ? & ?). exists (element B). exact _.
  }
  setoid_rewrite in_fun_replacement_iff.
  automation.
Qed.
Global Opaque indexed_union.
Hint Rewrite in_indexed_union_iff : sets.

Instance in_indexed_union x (A : S) (f : A -> S) (a : A) :
  x ∈ f a ->
  x ∈ ⋃ a ∈ A, f a.
Proof. automation. Qed.

Definition indexed_intersection (A : S) (f : A -> S) (_ : inhabited A) :=
  `{ z in ⋃ x ∈ A, f x | forall x : A, z ∈ f x }.

Notation "⋂ x ∈ A , y" := (indexed_intersection A (fun x => y) _)
                            (at level 60, x ident).

Program Lemma in_indexed_intersection_iff
        (A : S) (f : A -> S) (x : inhabited A) z :
  (z ∈ ⋂ x ∈ A, f x) <-> (forall x : A, z ∈ f x).
Proof.
  destruct x as [x].
  unfold indexed_intersection.
  rewrite in_comprehension_iff; cbn.
  split.
  - automation.
  - intros H. eexists.
    + rewrite in_indexed_union_iff.
      eexists. apply H.
      Unshelve.
      exact x.
    + automation.
Qed.
Global Opaque indexed_intersection.
Hint Rewrite in_indexed_intersection_iff : sets.

Program Definition intersection A B :=
  ⋂ C ∈ `{A, B}, C.
Next Obligation. refine (inhabits (element A)). automation. Qed.
(* At the same level as * *)
Notation "A ∩ B" := (intersection A B) (at level 40).

Lemma in_intersection_iff x A B :
  x ∈ A ∩ B <-> x ∈ A /\ x ∈ B.
Proof.
  unfold intersection. rewrite in_indexed_intersection_iff.
  split.
  - intros H.
    split.
    + refine (H (element A)). automation.
    + refine (H (element B)). automation.
  - automation.
Qed.
Global Opaque intersection.
Hint Rewrite in_intersection_iff : sets.

Definition difference x y :=
  `{ u in x | u ∉ y }.
Notation "x \ y" := (difference x y) (at level 50, left associativity).

Lemma in_difference_iff x y z :
  x ∈ y \ z <-> x ∈ y /\ x ∉ z.
Proof. unfold difference. rewrite in_comprehension_iff; cbn. firstorder. Qed.
Global Opaque difference.
Hint Rewrite in_difference_iff : sets.

Hint Unfold uniqueness : core.

Class Is_Unique_Solution_Of {A : Class} (a : A) (P : A -> Prop) : Type :=
  build_is_unique_solution {
      unique_solution_is_solution : P a;
      unique_solution_is_unique : forall x, P x -> x = a
    }.
Arguments build_is_unique_solution {_} _ _ _.
Arguments unique_solution_is_solution {_ _ _} _.
Arguments unique_solution_is_unique {_ _ _} _.

Existing Class unique.

Section Description.

  Context {A : Class}.
  Context (P : A -> Prop).
  Context (x : exists! x, P x).

  Program Definition solutions :=
    replacement (fun _ y => exists (H : y ∈ A), P (element y)) _ `{∅}.
  Next Obligation.
    intros _ y y'.
    intros [y_in_A P_y] [y'_in_A P_y'].
    unfold unique in *. destruct x as (x' & P_x & uniqueness).
    change (element y = element y' :> S).
    setoid_rewrite <- (uniqueness (element y) P_y).
    setoid_rewrite <- (uniqueness (element y') P_y').
    reflexivity.
  Qed.

  Program Definition description : A :=
    element (big_union solutions).
  Next Obligation.
    destruct x as (x' & P_x & uniqueness).
    replace solutions with (`{x' : S}). {
      replace (big_union `{x' : S}) with (x' : S). {
        exact _.
      }
      apply extensionality; intros y.
      rewrite in_big_union_iff. split.
      - intros y_in_x.
        assert (x' ∈ `{x' : S}) by automation.
        exists (element x'). exact y_in_x.
      - intros [[B HB] y_in_B].
        assert (B = x') as -> by automation.
        exact y_in_B.
    }
    apply extensionality; intros y.
    unfold solutions. simplify. split.
    - intros [-> | []].
      assert (∅ ∈ `{∅}) by automation.
      exists (element ∅), _. rewrite strip_element. exact P_x.
    - intros (_ & y_in_A & P_y). left.
      rewrite (uniqueness (element y) P_y). reflexivity.
  Qed.

  Instance description_is_unique :
    unique P description.
  Proof.
    destruct x as (x' & P_x & uniqueness).
    unfold description.
    replace (element (big_union _)) with x'. {
      split.
      - exact P_x.
      - exact uniqueness.
    }
    apply element_equality; cbn.
    transitivity (big_union `{x' : S}). {
      apply extensionality; intros y.
      rewrite in_big_union_iff. split.
      - intros y_in_x.
        assert (x' ∈ `{x' : S}) by automation.
        exists (element x'). exact y_in_x.
      - intros [[B HB] y_in_B].
        assert (B = x') as -> by automation.
        exact y_in_B.
    }
    f_equal.
    apply extensionality; intros y.
    unfold solutions. simplify. split.
    - intros [-> | []].
      assert (∅ ∈ `{∅}) by automation.
      exists (element ∅), _. rewrite strip_element. exact P_x.
    - intros (_ & y_in_A & P_y). left.
      rewrite (uniqueness (element y) P_y). reflexivity.
  Qed.

  Global Opaque description.

  Lemma description_is_solution :
    P (description).
  Proof. destruct description_is_unique. assumption. Qed.

End Description.

Notation "'δ' x : A , P" :=
  (description (fun x : A => P) _)
    (at level 200, x ident, P at level 200).

Notation σ x := (x @ x).

Fixpoint nat_to_numeral' n :=
  match n with
  | 0 => ∅
  | Datatypes.S n => σ (nat_to_numeral' n)
  end.
Parameter Numeral : S.
Axiom in_Numeral_iff' :
  forall x, x ∈ Numeral <-> exists n, x = nat_to_numeral' n.

Program Definition numeral_O : Numeral := element ∅.
Next Obligation. rewrite in_Numeral_iff'. exists 0. reflexivity. Qed.

Program Definition numeral_S (n : Numeral) : Numeral :=
  element (σ n).
Next Obligation.
  rewrite in_Numeral_iff'.
  assert (H : n ∈ Numeral) by exact _.
  rewrite in_Numeral_iff' in H. destruct H as [m H].
  exists (1 + m). rewrite H. reflexivity.
Qed.

Fixpoint nat_to_numeral (n : nat) : Numeral :=
  match n with
  | 0 => numeral_O
  | Datatypes.S n => numeral_S (nat_to_numeral n)
  end.
Coercion nat_to_numeral : nat >-> Element_Of.
Arguments nat_to_numeral : simpl never.

Lemma nat_to_numeral_is_nat_to_numeral' (n : nat) :
  n = nat_to_numeral' n :> S.
Proof.
  induction n; cbn [nat_to_numeral'].
  - reflexivity.
  - rewrite <- IHn. reflexivity.
Qed.

Lemma in_Numeral_iff x :
  x ∈ Numeral <-> exists n, x = nat_to_numeral n.
Proof.
  rewrite in_Numeral_iff'.
  setoid_rewrite nat_to_numeral_is_nat_to_numeral'.
  reflexivity.
Qed.
Hint Rewrite in_Numeral_iff.

Lemma nat_to_numeral_is_monotone (n n' : nat) :
  n < n' -> n ∈ n'.
Proof. intros lt. induction lt; automation. Qed.

Lemma nat_to_numeral_is_injective {n n' : nat} :
  n = n' :> Numeral ->
  n = n'.
Proof.
  intros H.
  destruct (lt_eq_lt_dec n n') as [[? | ?] | ?].
  - assert (H' : n ∈ n'). {
      apply nat_to_numeral_is_monotone.
      assumption.
    }
    rewrite H in H'. apply no_set_contains_itself in H'. contradiction.
  - assumption.
  - assert (H' : n' ∈ n). {
      apply nat_to_numeral_is_monotone.
      assumption.
    }
    rewrite H in H'. apply no_set_contains_itself in H'. contradiction.
Qed.

Definition Numeral_ind (P : Numeral -> Prop) :
  P O ->
  (forall n, P n -> P (numeral_S n)) ->
  forall n, P n.
Proof.
  intros base step n.
  pose (_ : n ∈ Numeral) as n_in_Numeral.
  rewrite in_Numeral_iff in n_in_Numeral.
  destruct n_in_Numeral as [n0 ->%element_equality].
  induction n0; cbn.
  - exact base.
  - apply step.
    exact IHn0.
Qed.

Definition Numeral_iter_Property {A : Class}
           (base : A) (step : Numeral -> A -> A) (n : Numeral) (a : A) :=
  forall n0 : nat, n = n0 -> a = nat_rect _ base step n0.

Program Definition Numeral_iter {A : Class}
        (base : A) (step : Numeral -> A -> A) (n : Numeral) : A :=
  δ a : A, Numeral_iter_Property base step n a.
Next Obligation.
  assert (H : n ∈ Numeral) by exact _. rewrite in_Numeral_iff in H.
  destruct H as [n0 ->%element_equality].
  exists (nat_rect _ base step n0).
  split.
  - intros n1 ->%nat_to_numeral_is_injective.
    reflexivity.
  - intros a H.
    symmetry.
    apply H.
    reflexivity.
Qed.

Lemma Numeral_iter_property {A : S}
           (base : A) (step : Numeral -> A -> A) (n : Numeral) :
  Numeral_iter_Property base step n
                        (Numeral_iter base step n).
Proof. unfold Numeral_iter. apply description_is_unique. Qed.
Global Opaque Numeral_iter.

Lemma Numeral_iter_reduction_O {A : S}
       (step : Numeral -> A -> A) (base : A) :
  Numeral_iter base step numeral_O = base.
Proof. apply (Numeral_iter_property base step numeral_O 0). reflexivity. Qed.
Hint Rewrite @Numeral_iter_reduction_O : sets.

Lemma Numeral_iter_reduction_S {A : S}
      (n : Numeral) (step : Numeral -> A -> A) (base : A) :
  Numeral_iter base step (numeral_S n) = step n (Numeral_iter base step n).
Proof.
  assert (Hn : n ∈ Numeral) by exact _.
  rewrite in_Numeral_iff in Hn. destruct Hn as [n0 ->%element_equality].
  rewrite (Numeral_iter_property base step (numeral_S n0) (1 + n0)). {
    rewrite (Numeral_iter_property base step n0 n0). {
      reflexivity.
    }
    reflexivity.
  }
  reflexivity.
Qed.
Hint Rewrite @Numeral_iter_reduction_S : sets.

Lemma one_ind (P : 1 -> Prop) :
  P (element 0) -> forall x : 1, P x.
Proof.
  intros H x.
  assert (Hx : x ∈ 1) by exact _. change (x ∈ 0 @ ∅) in Hx. simplify.
  destruct Hx as [Hx | []].
  replace x with (element 0). {
    exact H.
  }
  apply element_equality. symmetry. exact Hx.
Qed.

Definition untyped_pair x y :=
  `{`{x}, `{x, y}}.

Lemma untyped_pair_is_injective_left {x x' y y' : S} :
  untyped_pair x y = untyped_pair x' y'->
  x = x'.
Proof. unfold untyped_pair. automation. Qed.

Lemma untyped_pair_is_injective_right (x x' y y' : S) :
  untyped_pair x y = untyped_pair x' y' ->
  y = y'.
Proof. unfold untyped_pair. automation. Qed.

Definition cartesian_product A B :=
  ⋃ x ∈ A, ⋃ y ∈ B, `{ untyped_pair x y }.
Notation "x × y" := (cartesian_product x y) (at level 40, left associativity).

Program Definition pair {A B : S} (x : A) (y : B) : A × B :=
  element (untyped_pair x y).
Next Obligation.
  unfold cartesian_product.
  rewrite in_indexed_union_iff. exists (element x).
  rewrite in_indexed_union_iff. exists (element y).
  rewrite in_explicit_set_iff; cbn. tauto.
Qed.
Notation "`( x , y )" := (pair x y).

Lemma pair_is_injective_right {A B : S} {x x' : A} {y y' : B} :
  `(x, y) = `(x', y') ->
  y = y'.
Proof.
  intros H. apply element_equality. apply element_equality in H.
  apply untyped_pair_is_injective_right in H. exact H.
Qed.

Lemma pair_is_injective_left {A B : S} {x x' : A} {y y' : B} :
  `(x, y) = `(x', y') ->
  x = x'.
Proof.
  intros H. apply element_equality. apply element_equality in H.
  apply untyped_pair_is_injective_left in H. exact H.
Qed.

Program Definition left_projection {A B : S} (z : A × B) : A :=
  δ x : A, exists y, z = `(x, y).
Next Obligation.
  assert (Hz : z ∈ A × B) by exact _.
  unfold cartesian_product in Hz.
  rewrite in_indexed_union_iff in Hz. destruct Hz as [a Hz].
  rewrite in_indexed_union_iff in Hz. destruct Hz as [b Hz].
  rewrite in_explicit_set_iff in Hz; cbn in Hz. destruct Hz as [Hz | []].
  exists a. split.
  - exists b. apply element_equality. exact Hz.
  - intros a' [b' ->]. apply untyped_pair_is_injective_left in Hz.
    symmetry. apply element_equality. exact Hz.
Qed.
Notation "'π1'" := left_projection.

Lemma left_projection_beta {A B : S} (x : A) (y : B) :
  π1 `(x, y) = x.
Proof.
  assert (H : exists y', `(x, y) = `(π1 `(x, y), y')). {
    unfold left_projection. apply description_is_solution.
  }
  destruct H as [y' H]. apply pair_is_injective_left in H.
  symmetry. exact H.
Qed.
Hint Rewrite @left_projection_beta : sets.

Program Definition right_projection {A B : S} (z : A × B) : B :=
  δ y : B, exists x, z = `(x, y).
Next Obligation.
  assert (Hz : z ∈ A × B) by exact _.
  unfold cartesian_product in Hz.
  rewrite in_indexed_union_iff in Hz. destruct Hz as [a Hz].
  rewrite in_indexed_union_iff in Hz. destruct Hz as [b Hz].
  rewrite in_explicit_set_iff in Hz; cbn in Hz. destruct Hz as [Hz | []].
  exists b. split.
  - exists a. apply element_equality. exact Hz.
  - intros b' [a' ->]. apply untyped_pair_is_injective_right in Hz.
    symmetry. apply element_equality. exact Hz.
Qed.
Notation "'π2'" := right_projection.

Lemma right_projection_beta {A B : S} (x : A) (y : B) :
  π2 `(x, y) = y.
Proof.
  assert (H : exists x', `(x, y) = `(x', π2 `(x, y))). {
    unfold right_projection. apply description_is_solution.
  }
  destruct H as [y' H]. apply pair_is_injective_right in H.
  symmetry. exact H.
Qed.
Hint Rewrite @right_projection_beta : sets.

Lemma cartesian_product_eta {A B : S} (z : A × B) :
  `(π1 z, π2 z) = z.
Proof.
  assert (H1 : exists a b, z = `(a, b)). {
    assert (H2 : z ∈ A × B) by exact _. unfold cartesian_product in H2.
    rewrite in_indexed_union_iff in H2. destruct H2 as [a H2]. exists a.
    rewrite in_indexed_union_iff in H2. destruct H2 as [b H2]. exists b.
    rewrite in_explicit_set_iff in H2; cbn in H2. destruct H2 as [H2 | []].
    apply element_equality. exact H2.
  } destruct H1 as (a & b & ->).

  simplify. reflexivity.
Qed.
Hint Rewrite @cartesian_product_eta : sets.

Lemma cartesian_product_upper_bound {A : S} :
  A × A ⊆ 𝒫 (𝒫 A).
Proof.
  intros x.
  rewrite in_power_set_iff. intros Hx.
  change x with (element x : S). rewrite <- (cartesian_product_eta (element x)).
  unfold pair. unfold untyped_pair; cbn.
  automation.
Qed.

Global Opaque pair cartesian_product left_projection right_projection.

Definition disjoint_union (A B : S) :=
  `{ `(0, a) | a in A } ∪
  `{ `(1, b) | b in B }.
Notation "A ⊔ B" := (disjoint_union A B) (at level 50, left associativity).

Program Definition inj1 (A B : S) (x : A) : A ⊔ B :=
  element `(0, x).

Program Definition inj2 (A B : S) (x : B) : A ⊔ B :=
  element `(1, x).

Lemma inj1_is_injective (A B : S) (a a' : A) :
  inj1 A B a = inj1 A B a' ->
  a = a'.
Proof.
  intros ?.
  assert (H1 : `(0, a) = `(0, a')). {
    apply element_equality. apply element_equality in H. exact H.
  }
  apply pair_is_injective_right in H1. exact H1.
Qed.

Lemma inj2_is_injective (A B : S) (b b' : B) :
  inj2 A B b = inj2 A B b' ->
  b = b'.
Proof.
  intros ?.
  assert (H1 : `(1, b) = `(1, b')). {
    apply element_equality. apply element_equality in H. exact H.
  }
  apply pair_is_injective_right in H1. exact H1.
Qed.

Lemma inj1_and_inj2_are_disjoint (A B : S) (a : A) (b : B) :
  inj1 A B a <> inj2 A B b.
Proof.
  rewrite <- element_equality; cbn.
  intros H.
  assert (0 = 1 :> Numeral). {
    apply untyped_pair_is_injective_left in H.
    apply element_equality in H.
    assumption.
  }
  assert (0 = 1 :> nat). {
    apply nat_to_numeral_is_injective.
    assumption.
  }
  discriminate.
Qed.

Definition Disjoint_Union_Iter_Property {A B : S} {C : Class}
        (l_step : A -> C) (r_step : B -> C) (x : A ⊔ B) (c : C) :=
  (forall a : A, x = inj1 A B a -> c = l_step a) /\
  (forall b : B, x = inj2 A B b -> c = r_step b).

Program Definition disjoint_union_iter {A B : S} {C : Class}
        (l_step : A -> C) (r_step : B -> C) (x : A ⊔ B) : C :=
  δ c : C, Disjoint_Union_Iter_Property l_step r_step x c.
Next Obligation.
  assert (Hx : x ∈ A ⊔ B) by exact _.
  unfold disjoint_union in Hx. simplify.
  change ((exists a, x = inj1 A B a :> S) \/ (exists b, x = inj2 A B b :> S)) in Hx.
  destruct Hx as [[a ->%element_equality] | [b ->%element_equality]].
  - exists (l_step a). split.
    + split.
      * intros a' ->%inj1_is_injective. reflexivity.
      * intros b H.
        exfalso. eapply inj1_and_inj2_are_disjoint. exact H.
    + intros c [H1 H2]. symmetry. apply H1. reflexivity.
  - exists (r_step b). split.
    + split.
      * intros a H.
        exfalso. eapply inj1_and_inj2_are_disjoint. symmetry. exact H.
      * intros b' ->%inj2_is_injective. reflexivity.
    + intros c [H1 H2]. symmetry. apply H2. reflexivity.
Qed.

Lemma disjoint_union_iter_property {A B : S} {C : S}
      (l_step : A -> C) (r_step : B -> C) (x : A ⊔ B) :
  Disjoint_Union_Iter_Property l_step r_step x
                               (disjoint_union_iter l_step r_step x).
Proof.
  unfold disjoint_union_iter.
  apply description_is_solution.
Qed.

Lemma disjoint_union_iter_reduction_left {A B : S} {C : S}
      (a : A) (l_step : A -> C) (r_step : B -> C) :
  disjoint_union_iter l_step r_step (inj1 A B a) = l_step a.
Proof. apply disjoint_union_iter_property. reflexivity. Qed.
Hint Rewrite @disjoint_union_iter_reduction_left : sets.

Lemma disjoint_union_iter_reduction_right {A B : S} {C : S}
      (b : B) (l_step : A -> C) (r_step : B -> C) :
  disjoint_union_iter l_step r_step (inj2 A B b) = r_step b.
Proof. apply disjoint_union_iter_property. reflexivity. Qed.
Hint Rewrite @disjoint_union_iter_reduction_right : sets.

Definition disjoint_union_ind {A B : S} (P : A ⊔ B -> Prop) :
  (forall a : A, P (inj1 A B a)) ->
  (forall b : B, P (inj2 A B b)) ->
  forall x : A ⊔ B, P x.
Proof.
  intros left_step right_step x.
  assert (H : x ∈ A ⊔ B) by exact _. unfold disjoint_union in H.
  simplify.
  destruct H as [[a e] | [b e]].
  - change (x = inj1 A B a :> S) in e. rewrite element_equality in e.
    rewrite e. apply left_step.
  - change (x = inj2 A B b :> S) in e. rewrite element_equality in e.
    rewrite e. apply right_step.
Qed.

Lemma two_times_set_is_disjoin_union A :
  2 × A = A ⊔ A.
Proof.
  unfold disjoint_union.
  apply extensionality; intros x. split.

  - intros ?.
    change x with (element_value (element x)).
    rewrite <- cartesian_product_eta at 1.
    set (i := π1 (element x)).
    set (a := π2 (element x)).
    assert (i_in_2 : i ∈ 2) by exact _.
    change (i ∈ `{(1 : S), (0 : S)}) in i_in_2. simplify.
    change (1 : S) with ((element 1 : 2) : S) in i_in_2.
    change (0 : S) with ((element 0 : 2) : S) in i_in_2.
    destruct i_in_2 as [->%element_equality | [->%element_equality | []]].
    + right. exists a. reflexivity.
    + left. exists a. reflexivity.

  - simplify. intros [[a ->] | [a ->]].
    + change (`(0, a) : S) with (`(element 0 : 2, a) : S). exact _.
    + change (`(1, a) : S) with (`(element 1 : 2, a) : S). exact _.

Qed.



Global Opaque inj1 inj2 disjoint_union disjoint_union_iter.

Definition Is_From_Left {A B} (x : A ⊔ B) :=
  exists a : A, x = inj1 _ _ a.

Definition extract_from_left {A B} (x : A ⊔ B) `{H : Is_From_Left x} :
  A.
Proof.
  unfold Is_From_Left in H.
  refine (δ a : A, x = inj1 A B a).
  destruct H as [a ->].
  exists a. split.
  - reflexivity.
  - apply inj1_is_injective.
Defined.

Program Lemma inj1_extract_from_left {A B} (x : A ⊔ B) `{Is_From_Left x} :
  inj1 _ _ (extract_from_left x) = x.
Proof.
  unfold extract_from_left. symmetry. apply description_is_solution.
Qed.

Definition Is_From_Right {A B} (x : A ⊔ B) :=
  exists b : B, x = inj2 _ _ b.

Definition extract_from_right {A B} (x : A ⊔ B) `{H : Is_From_Right x} :
  B.
Proof.
  unfold Is_From_Right in H.
  refine (δ b : B, x = inj2 A B b).
  destruct H as [b ->].
  exists b. split.
  - reflexivity.
  - apply inj2_is_injective.
Defined.

Program Lemma extract_from_right_is_injective {A B} (x x' : A ⊔ B)
      `{H : Is_From_Right x} `{H' : Is_From_Right x'} :
  extract_from_right x = extract_from_right x' ->
  x = x'.
Proof.
  intros H1.
  transitivity (inj2 A B (@extract_from_right _ _ x H)). {

    unfold extract_from_right. apply description_is_solution.
  }
  transitivity (inj2 A B (@extract_from_right _ _ x' H')). {

    congruence.
  }
  unfold extract_from_right. symmetry. apply description_is_solution.
Qed.

Lemma from_left_or_right {A B} (x : A ⊔ B) :
  Is_From_Left x \/ Is_From_Right x.
Proof.
  revert x. apply disjoint_union_ind.
  - left. unfold Is_From_Left. exists a. reflexivity.
  - right. unfold Is_From_Right. exists b. reflexivity.
Qed.