Require Export Sierpinski.Basics.
Unset Printing Records.

Require Import Coq.Logic.Classical.

Require Import Coq.Program.Program.
Require Import Coq.Setoids.Setoid.

Definition Less_Or_Equal {A} {R : relation A} `{PreOrder A R} (x y : A) :=
  R x y.

Notation "x <= y" := (Less_Or_Equal x y).
Notation "A <= B <= C" := (A <= B /\ B <= C).

Record Bijection A B :=
  build_bijection {
      bijection_to_right :> A -> B;
      bijection_to_left : B -> A;
      bijection_right_left : forall a, bijection_to_left (bijection_to_right a) = a;
      bijection_left_right : forall b, bijection_to_right (bijection_to_left b) = b;
    }.
Arguments build_bijection {_ _} _ _ _ _.
Arguments bijection_to_right {_ _} _.
Arguments bijection_to_left {_ _} _.
Arguments bijection_right_left {_ _} _.
Arguments bijection_left_right {_ _} _.

Program Definition id_bijection (A : Type) : Bijection A A :=
  build_bijection id id _ _.

Definition inverse_bijection {A B} (f : Bijection A B) : Bijection B A :=
  build_bijection (bijection_to_left f)
                  (bijection_to_right f)
                  (bijection_left_right f)
                  (bijection_right_left f).
Notation "f ⁻¹" := (inverse_bijection f) (at level 5, format "f ⁻¹").
Arguments inverse_bijection {_ _} !_.

Lemma cancel_inverse_right {A B} (f : Bijection A B) (x : B) :
  f (f⁻¹ x) = x.
Proof. apply bijection_left_right. Qed.
Hint Rewrite @cancel_inverse_right : sets.

Lemma cancel_inverse_left {A B} (f : Bijection A B) (x : A) :
  f⁻¹ (f x) = x.
Proof. apply bijection_left_right. Qed.
Hint Rewrite @cancel_inverse_left : sets.

Program Definition compose_bijections {A B C}
           (f1 : Bijection B C) (f2 : Bijection A B) :
  Bijection A C :=
  build_bijection (f1 ∘ f2)
                  (f2⁻¹ ∘ f1⁻¹)
                  _ _.
Next Obligation.
  unfold compose.
  repeat rewrite bijection_right_left. reflexivity.
Qed.
Next Obligation.
  unfold compose.
  repeat rewrite bijection_left_right. reflexivity.
Qed.

Lemma inverse_compose_function {A B} (f : Bijection A B) :
  f⁻¹ ∘ f = id.
Proof.
  apply functional_extensionality; intros a. unfold compose, id.
  apply cancel_inverse_left.
Qed.

Lemma function_compose_inverse {A B} (f : Bijection A B) :
  f ∘ f⁻¹ = id.
Proof.
  apply functional_extensionality; intros a. unfold compose, id.
  apply cancel_inverse_right.
Qed.

Definition bijection_relation A B : Prop :=
  inhabited (Bijection A B).
Definition bijection_relation_on_Set (A B : S) : Prop :=
  inhabited (Bijection A B).
Notation "A ∼ B" := (bijection_relation_on_Set A B) (at level 70).

Lemma bijection_relation_reflexivity A :
  A ∼ A.
Proof. exact (inhabits (id_bijection A)). Qed.

Lemma bijection_relation_symmetry A B :
  A ∼ B ->
  B ∼ A.
Proof. intros [f]. exact (inhabits f⁻¹). Qed.

Lemma bijection_relation_transitivity A B C :
  A ∼ B ->
  B ∼ C ->
  A ∼ C.
Proof. intros [f] [g]. exact (inhabits (compose_bijections g f)). Qed.

Global Add Relation S bijection_relation
    reflexivity proved by bijection_relation_reflexivity
    symmetry proved by bijection_relation_symmetry
    transitivity proved by bijection_relation_transitivity
      as bijection_is_equivalence.

Record Injection A B :=
  build_injection {
      injection_fun :> A -> B;
      injection_property : injective injection_fun
    }.
Arguments build_injection {_ _} _ _.
Arguments injection_fun {_ _} _.
Arguments injection_property {_ _} _.
Notation "A ↪ B" := (Injection A B) (at level 99).

Program Definition id_injection A : A ↪ A :=
  build_injection id _.
Next Obligation.
  intros a a' H. apply H.
Qed.

Program Definition compose_injections {A B C}
        (f : B ↪ C) (g : A ↪ B) :
  A ↪ C :=
  build_injection (f ∘ g) _.
Next Obligation.
  intros a a' H.
  apply injection_property in H.
  apply injection_property in H.
  exact H.
Qed.

Lemma bijection_is_injective {A B} (f : Bijection A B) :
  injective f.
Proof.
  intros a a' H.
  assert (H1 : f⁻¹ (f a) = f⁻¹ (f a')) by congruence.
  repeat rewrite cancel_inverse_left in H1.
  assumption.
Qed.

Lemma bijection_to_injection {A B} (f : Bijection A B) : A ↪ B.
Proof.
  refine (build_injection f _).
  apply bijection_is_injective.
Qed.

Program Definition injection_as_bijection_into_image {A B : S} (f : A ↪ B) :
  Bijection A (image_of f).
Proof.

  unshelve eset (h (x : A) := element (f x) : image_of f).

  unshelve eset (h' (y : image_of f) := δ x : A, f x = y :> S). {
    assert (H : y ∈ image_of f) by exact _. unfold image_of in H; cbn in H.
    rewrite in_fun_replacement_iff in H. destruct H as [x H].
    exists x. split.
    - symmetry. exact H.
    - intros x' H'. apply (injection_property f).
      apply element_equality. rewrite <- H. rewrite H'. reflexivity.
  }

  refine (build_bijection h h' _ _).
  - unfold h', h; cbn. intros a. apply (injection_property f).
    apply element_equality. apply description_is_solution.
  - unfold h, h'. intros b.
    apply element_equality; cbn. apply description_is_solution.
Defined.

Definition injection_relation A B : Prop :=
  inhabited (A ↪ B).

Definition injection_relation_on_Set (A B : S) : Prop :=
  inhabited (A ↪ B).

Lemma injection_relation_reflexivity A :
  injection_relation A A.
Proof. exact (inhabits (id_injection A)). Qed.

Lemma injection_relation_transitivity A B C :
  injection_relation A B ->
  injection_relation B C ->
  injection_relation A C.
Proof. intros [f] [g]. exact (inhabits (compose_injections g f)). Qed.

Add Relation Class injection_relation
    reflexivity proved by injection_relation_reflexivity
    transitivity proved by injection_relation_transitivity
      as injection_relation_is_preorder.

Add Relation S injection_relation_on_Set
    reflexivity proved by injection_relation_reflexivity
    transitivity proved by injection_relation_transitivity
      as injection_relation_on_Set_is_preorder.

Instance subset_subrelation_injection :
  subrelation (Is_Subclass_Of : relation S) injection_relation_on_Set.
Proof.
  intros A B AB.
  simple refine (inhabits (build_injection _ _)).
  - intros x.
    assert (x ∈ B). {
      apply AB. exact _.
    }
    exact (element x).
  - intros a a'. cbn. setoid_rewrite <- element_equality. tauto.
Qed.

Instance bijection_subrelation_injection :
  subrelation bijection_relation_on_Set injection_relation_on_Set.
Proof.
  unfold subrelation. intros A B [f].
  apply inhabits. exact (bijection_to_injection f).
Qed.

Instance bijection_subrelation_flipped_injection :
  subrelation bijection_relation_on_Set (flip injection_relation_on_Set).
Proof.
  unfold subrelation. intros A B H. unfold flip.
  rewrite <- H. reflexivity.
Qed.

Lemma image_of_injection_is_equipotent {A B : S} (f : A ↪ B) :
  image_of f ∼ A.
Proof.
  symmetry.
  apply inhabits.
  exact (injection_as_bijection_into_image f).
Qed.

Add Morphism power_set
    with signature bijection_relation_on_Set ==> bijection_relation_on_Set
      as power_set_bijection_mor.
Proof.
  intros A B [f].
  refine (inhabits (build_bijection (image_under f)
                                    (image_under f⁻¹)
                                    _ _)).
  - intros A'. rewrite image_of_image.
    rewrite inverse_compose_function. apply image_under_id.
  - intros B'. rewrite image_of_image.
    rewrite function_compose_inverse. apply image_under_id.
Qed.

Add Morphism power_set
    with signature injection_relation_on_Set ==> injection_relation_on_Set
      as power_set_injection_mor.
Proof.
  intros A B [f].
  refine (inhabits (build_injection (image_under f) _)).
  intros A1 A2 H1.
  apply subset_extensionality; intros a.
  transitivity (f a ∈ f '' A1). {
    rewrite in_image_iff. firstorder.
    apply injection_property in H0. rewrite H0. assumption.
  }
  transitivity (f a ∈ f '' A2). {
    rewrite H1. reflexivity.
  }
  rewrite in_image_iff. firstorder.
  apply injection_property in H0. rewrite H0. assumption.
Qed.

Lemma power_set_is_increasing (A : S) :
  A <= 𝒫 A.
Proof.
  simple refine (inhabits (build_injection (fun x : A => element `{(x : S)}) _)).

  - automation.

  - intros x y. repeat rewrite <- element_equality; cbn.
    rewrite explicit_set_equals_explicit_set_iff; cbn.
    tauto.

Qed.

Add Morphism cartesian_product
    with signature injection_relation_on_Set ==> injection_relation_on_Set ==> injection_relation_on_Set
      as cartesian_product_injection_mor.
Proof.
  intros A A' [f] B B' [g].
  refine (inhabits (build_injection (fun x => `(f (π1 x), g (π2 x))) _)).
  intros x x'.
  intros H.
  pose (pair_is_injective_left H) as Hf. apply injection_property in Hf.
  pose (pair_is_injective_right H) as Hg. apply injection_property in Hg.
  rewrite <- cartesian_product_eta.
  rewrite <- Hf, <- Hg.
  rewrite cartesian_product_eta.
  reflexivity.
Qed.

Lemma symmetric_cartesian_product_is_increasing (A : S) :
  A <= A × A.
Proof.
  refine (inhabits (build_injection (fun a => `(a, a)) _)).
  intros a a' e. apply pair_is_injective_left in e. exact e.
Qed.

Add Parametric Morphism : disjoint_union
    with signature
    bijection_relation_on_Set ==> bijection_relation_on_Set ==> bijection_relation_on_Set
      as disjoint_union_bijection_mor.
Proof.
  intros A A' [f] B B' [g].

  set (h := disjoint_union_iter (inj1 _ _ ∘ f ) (inj2 _ _ ∘ g )).
  set (h' := disjoint_union_iter (inj1 _ _ ∘ f⁻¹) (inj2 _ _ ∘ g⁻¹)).

  refine (inhabits (build_bijection h h' _ _)).

  - apply disjoint_union_ind.
    + intros x. unfold h, h'. simplify. reflexivity.
    + intros x. unfold h, h'. simplify. reflexivity.

  - apply disjoint_union_ind.
    + intros x. unfold h, h'. simplify. reflexivity.
    + intros x. unfold h, h'. simplify. reflexivity.
Qed.

Add Morphism disjoint_union
    with signature injection_relation_on_Set ==> injection_relation_on_Set ==> injection_relation_on_Set
      as disjoint_union_injection_mor.
Proof.
  intros A A' [f] B B' [g].

  set (h := disjoint_union_iter (inj1 _ _ ∘ f) (inj2 _ _ ∘ g)).

  refine (inhabits (build_injection h _)).
  refine (@disjoint_union_ind A B _ _ _); intros x;
    refine (@disjoint_union_ind A B _ _ _); intros x'.
  - unfold h. simplify. intros H.
    apply inj1_is_injective in H. apply injection_property in H. congruence.
  - unfold h. simplify. intros H.
    apply inj1_and_inj2_are_disjoint in H. contradiction.
  - unfold h. simplify. intros H. symmetry in H.
    apply inj1_and_inj2_are_disjoint in H. contradiction.
  - unfold h. simplify. intros H.
    apply inj2_is_injective in H. apply injection_property in H. congruence.
Qed.

Lemma disjoint_union_associative (A B C : S) :
  A ⊔ (B ⊔ C) ∼ A ⊔ B ⊔ C.
Proof.

  set (h := disjoint_union_iter
              (fun a : A => inj1 _ _ (inj1 _ _ a))
              (disjoint_union_iter
                 (fun b : B => inj1 _ _ (inj2 _ _ b))
                 (fun c : C => inj2 _ _ c))).

  set (h' := disjoint_union_iter
               (disjoint_union_iter
                  (fun a : A => inj1 _ _ a)
                  (fun b : B => inj2 _ _ (inj1 _ _ b)))
               (fun c : C => inj2 _ _ (inj2 _ _ c))).

  refine (inhabits (build_bijection h h' _ _)).

  - unfold h, h'.
    apply disjoint_union_ind.
    + intros a. simplify. reflexivity.
    + apply disjoint_union_ind.
      * intros b. simplify. reflexivity.
      * intros c. simplify. reflexivity.

  - unfold h, h'.
    apply disjoint_union_ind.
    + apply disjoint_union_ind.
      * intros a. simplify. reflexivity.
      * intros b. simplify. reflexivity.
    + intros a. simplify. reflexivity.
Qed.

Lemma disjoint_union_is_increasing_on_left (A B : S) :
  A <= A ⊔ B.
Proof.
  refine (inhabits (build_injection (inj1 _ _) _)).
  intros a a'. apply inj1_is_injective.
Qed.

Lemma disjoint_union_is_increasing_on_right (A B : S) :
  B <= A ⊔ B.
Proof.
  refine (inhabits (build_injection (inj2 _ _) _)).
  intros a a'. apply inj2_is_injective.
Qed.

Lemma Numeral_equipotent_Numeral_plus_one :
  Numeral ∼ 1 ⊔ Numeral.
Proof.

  set (f := Numeral_iter (inj1 _ _ (element 0))
                         (fun n _ => inj2 _ _ n) :
              Numeral -> 1 ⊔ Numeral).

  set (g := disjoint_union_iter (const numeral_O)
                                numeral_S :
              1 ⊔ Numeral -> Numeral).

  refine (inhabits (build_bijection f g _ _)).
  - unfold f, g. apply Numeral_ind.
    + simplify. reflexivity.
    + intros n _. simplify. reflexivity.
  - unfold f, g. apply disjoint_union_ind.
    + apply one_ind. simplify. reflexivity.
    + intros n. simplify. reflexivity.
Qed.

Lemma set_equals_subset_union_difference (A B : S) :
    B ⊆ A ->
    A = B ∪ (A \ B).
Proof.
  intros H. apply extensionality. intros x.
  simplify. intuition; tauto.
Qed.

Definition Disjoint A B :=
  ~ exists x, x ∈ A /\ x ∈ B.

Lemma union_of_disjoints_equipotent_disjoint_union (A B : S) :
    Disjoint A B ->
    A ∪ B ∼ A ⊔ B.
Proof.
  intros H0.

  unshelve eset (f (x : A ∪ B) :=
                   δ y : A ⊔ B,
                         (forall H : x ∈ A, inj1 _ _ (element x) = y) /\
                         (forall H : x ∈ B, inj2 _ _ (element x) = y)). {
    
    assert (H1 : x ∈ A ∪ B) by exact _. rewrite in_union_iff in H1.
    destruct H1 as [H1 | H1].
    - exists (inj1 _ _ (element x)). split.
      + split.
        * intros H2. f_equal. apply element_equality. reflexivity.
        * intros H2. exfalso. firstorder.
      + intros x' [H2 H3]. apply H2.
    - exists (inj2 _ _ (element x)). split.
      + split.
        * intros H2. exfalso. firstorder.
        * intros H2. f_equal. apply element_equality. reflexivity.
      + intros x' [H2 H3]. apply H3.
  }

  assert (Hf : forall x : A ∪ B, (forall H : x ∈ A, inj1 _ _ (element x) = f x) /\
                            (forall H : x ∈ B, inj2 _ _ (element x) = f x)). {
    intros x. unfold f. apply description_is_solution.
  }


  unshelve set (g (x : A ⊔ B) :=
                  disjoint_union_iter (fun x : A => element x : A ∪ B)
                                      (fun x : B => element x : A ∪ B)
                                      x).

  simple refine (inhabits (build_bijection f g _ _)).
  - intros x.
    assert (H1 : x ∈ A ∪ B) by exact _. rewrite in_union_iff in H1. destruct H1.
    + rewrite <- (proj1 (Hf x) _).
      unfold g. simplify. apply element_equality. reflexivity.
    + rewrite <- (proj2 (Hf x) _).
      unfold g. simplify. apply element_equality. reflexivity.

  - apply disjoint_union_ind.
    + intros x. unfold g. simplify. rewrite <- (proj1 (Hf (element x)) _); cbn.
      rewrite strip_element. reflexivity.
    + intros x. unfold g. simplify. rewrite <- (proj2 (Hf (element x)) _); cbn.
      rewrite strip_element. reflexivity.
Qed.

Lemma set_equipotent_subset_plus_difference (A B : S) :
  B ⊆ A ->
  A ∼ B ⊔ (A \ B).
Proof.
  intros H.
  rewrite (set_equals_subset_union_difference A B) at 1.
  rewrite union_of_disjoints_equipotent_disjoint_union.
  reflexivity.

  - unfold Disjoint. automation.
  - assumption.
Qed.

Lemma set_equipotent_set_plus_one (A : S) :
    Numeral <= A ->
    A ∼ 1 ⊔ A.
Proof.
  intros [f].
  set (B := image_of f).

  transitivity (A). {
    reflexivity.
  }

  transitivity (B ⊔ (A \ B)). {

    apply set_equipotent_subset_plus_difference. automation.
  }

  transitivity (Numeral ⊔ (A \ B)). {
    unfold B.
    apply disjoint_union_bijection_mor.
    - exact (image_of_injection_is_equipotent f).
    - reflexivity.
  }

  transitivity (1 ⊔ Numeral ⊔ (A \ B)). {

    apply disjoint_union_bijection_mor.
    - exact Numeral_equipotent_Numeral_plus_one.
    - reflexivity.
  }

  transitivity (1 ⊔ B ⊔ (A \ B)). {
    
    apply disjoint_union_bijection_mor.
    - apply disjoint_union_bijection_mor.
      + reflexivity.
      + symmetry.
        apply image_of_injection_is_equipotent.
    - reflexivity.
  }

  transitivity (1 ⊔ (B ⊔ (A \ B))). {

    symmetry. apply disjoint_union_associative.
  }

  transitivity (1 ⊔ A). {

    apply disjoint_union_bijection_mor.
    - reflexivity.
    - symmetry.
      apply set_equipotent_subset_plus_difference. automation.
  }

  reflexivity.
Qed.

Lemma two_is_power_set_of_one :
  2 = 𝒫 1 :> S.
Proof.
  transitivity `{`{∅}, ∅}. reflexivity.
  apply extensionality. intros x. autorewrite with sets.
  cbn. split.

  - automation.
  - intros H.
    destruct (classic (∅ ∈ x)).
    + left. change (x = 1). apply extensionality; intros y; split.
      * automation.
      * intros ?. refine (one_ind (fun y => y ∈ x) _ (element y)). assumption.
    + right. left. apply extensionality. intros y. split.
      * intros ?. assert (y ∈ ∅ @ ∅). {
          apply H.
          exact _.
        }
        automation.
      * automation.
Qed.

Lemma power_set_of_disjoint_union (A B : S) :
  𝒫 (A ⊔ B) ∼ 𝒫 A × 𝒫 B.
Proof.

  unshelve eset (f (x : 𝒫 (A ⊔ B)) :=
                   `(`{ a in A | inj1 A B a ∈ x },
                     `{ b in B | inj2 A B b ∈ x })).

  unshelve eset (g (x : 𝒫 A × 𝒫 B) :=
                   element (inj1 A B '' π1 x ∪ inj2 A B '' π2 x)
                   : 𝒫 (A ⊔ B)). {
    rewrite in_power_set_iff; intros y. unfold image_under; cbn. simplify.
    intros [[a ->] | [b ->]]; exact _.
  }

  refine (inhabits (build_bijection f g _ _)).

  - intros x.
    apply subset_extensionality; intros y; cbn.
    unfold f. simplify. setoid_rewrite in_comprehension_iff_typed.
    split.
    + intros [(u & ? & ->) | (u & ? & ->)]; assumption.
    + revert y. refine (disjoint_union_ind _ _ _); automation.

  - intros x. unfold f. rewrite <- (cartesian_product_eta x) at 1.
    unfold g; cbn. f_equal.

    + apply subset_extensionality; intros a. unfold g. simplify.
      split.
      * intros [(a' & ? & H) | (b' & ? & H)].
        -- apply inj1_is_injective in H. rewrite H. assumption.
        -- apply inj1_and_inj2_are_disjoint in H. contradiction.
      * intros ?. left. exists a. automation.
    + apply subset_extensionality; intros b. unfold g. simplify.
      split.
      * intros [(a' & ? & H) | (b' & ? & H)].
        -- symmetry in H. apply inj1_and_inj2_are_disjoint in H. contradiction.
        -- apply inj2_is_injective in H. rewrite H. assumption.
      * intros ?. right. exists b. automation.
Qed.

Lemma power_set_equiv_power_set_plus_power_set A :
    Numeral <= A ->
    𝒫 A ∼ 𝒫 A ⊔ 𝒫 A.
Proof.
  intros ?.

  transitivity (𝒫 A). {

    reflexivity.
  }

  transitivity (𝒫 (1 ⊔ A)). {

    rewrite <- set_equipotent_set_plus_one.
    reflexivity.

    assumption.
  }

  transitivity (𝒫 1 × 𝒫 A). {

    apply power_set_of_disjoint_union.
  }


  transitivity (2 × 𝒫 A). {

    rewrite two_is_power_set_of_one.
    reflexivity.
  }
  
  transitivity (𝒫 A ⊔ 𝒫 A). {

    rewrite two_times_set_is_disjoin_union.
    reflexivity.
  }

  reflexivity.

Qed.

Record Surjection A B :=
  build_surjection {
      surjection_fun :> A -> B;
      surjection_is_surjective : surjective surjection_fun
    }.
Arguments build_surjection {_ _} _ _.
Arguments surjection_is_surjective {_ _}.
Notation "A ↠ B" := (Surjection A B) (at level 99).

Lemma cantors_theorem (A : S) :
  ~ inhabited (A ↠ 𝒫 A).
Proof.
  intros [f].

  unshelve eset (C := element `{ a in A | a ∉ f a } : 𝒫 A).

  assert (H : exists a : A, C = f a). {
    apply surjection_is_surjective.
  } destruct H as [a H].

  assert (a ∉ C). {
    intros H1.
    assert (H2 : a ∈ f a). {
      rewrite <- H. exact H1.
    }
    unfold C in H1; cbn in H1. rewrite in_comprehension_iff_typed in H1.
    contradiction.
  }


  assert (a ∈ C). {
    unfold C. cbn. rewrite in_comprehension_iff_typed.
    rewrite <- H. assumption.
  }


  contradiction.

Qed.

Definition Is_A_Set (A : Class) :=
  exists A' : S, forall x, x ∈ A <-> x ∈ A'.

Program Definition class_as_set (A : Class) (H : Is_A_Set A) : S :=
  δ A' : class_of_all_sets, forall x, x ∈ A <-> x ∈ A'.
Next Obligation.
  destruct H as [B H]. unfold unique. setoid_rewrite H. clear H.
  exists (element B); cbn. split.
  - reflexivity.
  - intros B' H'. apply element_equality. cbn.
    apply extensionality; intros x. apply H'.
Qed.

Lemma in_class_as_set_iff (A : Class) (H : Is_A_Set A) :
  forall x, x ∈ class_as_set A H <-> x ∈ A.
Proof.
  intros x. unfold class_as_set.
  symmetry. revert x. apply description_is_solution.
Qed.

Lemma class_as_set_equiv_set (A : Class) (H : Is_A_Set A) :
  bijection_relation (class_as_set A H) A.
Proof.
  simple refine (inhabits (build_bijection _ _ _ _)).
  - refine (fun x => element x). apply (in_class_as_set_iff A H). exact _.
  - refine (fun x => element x). apply in_class_as_set_iff. exact _.
  - cbn. setoid_rewrite strip_element. reflexivity.
  - cbn. setoid_rewrite strip_element. reflexivity.
Qed.

Lemma small_class_is_a_set (A : Class) (B : S) :
  A <= B ->
  Is_A_Set A.
Proof.
  intros [f].
  unshelve eexists `{ (δ x : A, f x = y) | y in B, exists x : A, f x = y }. {
    cbn. destruct e as [x <-].
    exists x. unfold unique. split.
    - reflexivity.
    - intros x' H. symmetry. apply (injection_property f). assumption.
  }
  intros x. rewrite in_conditional_fun_replacement_iff.
  split.
  - intros ?.
    exists (f (element x)).
    simple refine (ex_intro _ _ _).
    + exists (element x). reflexivity.
    + cbn. change x with (element x : S) at 1. rewrite element_equality.
      apply (injection_property f). symmetry. apply description_is_solution.
  - intros [y [[x' <-] ->]]. exact _.
Qed.