Problem1.v

Require Import Coq.Relations.Relations.
Require Import Coq.Sets.Constructive_sets.
Parameter X : Set.
Parameter Xle : relation X.
Axiom Xle_refl : reflexive _ Xle.
Axiom Xle_trans : transitive _ Xle.
Axiom Xle_antisym : antisymmetric _ Xle.

Notation "x =<= y" := (Xle x y) (at level 70, no associativity).

Definition XSle : relation (Ensemble X) :=
  fun S T =>
    Included _ S T /\
    forall a, In _ T a -> (exists2 x, In _ S x & a =<= x) -> In _ S a.

Notation "S <= T" := (XSle S T).

Parameter C : Ensemble (Ensemble X).
Axiom Ctotal: forall S T, In _ C S -> In _ C T -> S <= T \/ T <= S.

Definition CUnion : Ensemble X := fun x => exists2 S, In _ C S & In _ S x.

Parameter A : Ensemble X.
Axiom AinC : In _ C A.

Theorem Problem1: A <= CUnion.
Proof.
  split.
  - intros x H.
    exists A.
    + exact AinC.
    + exact H.
  - intros a [B HB Ha] [x Hx ax].
    destruct (Ctotal A B AinC HB) as [H|H].
    + apply (proj2 H _ Ha).
      exists x; assumption.
    + apply (proj1 H).
      assumption.
Qed.