Set Warnings "-extraction-opaque-accessed,-extraction".
Set Warnings "-notation-overridden,-parsing".

Require Import mathcomp.ssreflect.ssreflect.
Require Import Classes.RelationClasses Classes.Morphisms List Tactics.
From mathcomp Require Import ssrfun ssrbool ssrnat seq.

Import ListNotations.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

(* There are similar definitions in the Ensembles library (Included
   and Same_set); set_eq is not exactly the same as Same_set though
   (only logically equivalent). *)

Definition set T := T -> Prop.

Notation "x \in A" := (A x) (at level 70, only parsing) : set_scope.

Definition set_eq {A} (m1 m2 : set A) :=
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  forall (a : A), m1 a <-> m2 a.

Infix "<-->" := set_eq (at level 70, no associativity) : set_scope.

Open Scope set_scope.

Lemma set_eq_trans T B (A C : set T) : A <--> B -> B <--> C -> A <--> C.
Proof.
(* Goal: @set_eq A (@seq_In A (@cons A x l)) (@setU A (@set1 A x) (@seq_In A l)) *)
by move=> eqAB eqBC; split=> [/eqAB/eqBC|/eqBC/eqAB].
Qed.

Lemma set_eq_symm {A} (s1 s2 : set A) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  s1 <--> s2 -> s2 <--> s1.
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.

Lemma set_eq_refl {A} (s : set A) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  s <--> s.
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.


Global Instance : forall T, Equivalence (@set_eq T).
Proof.
(* Goal: and (A x) (@set_incl T (@seq_In T s) A) *)
move=> T; constructor=> // [A B eqAB | A B C] x; first by split=> /eqAB.
(* Goal: @set_eq U (@imset T U f (@set0 T)) (@set0 U) *)
exact: set_eq_trans.
Qed.

Definition set_incl {A} (m1 m2 : set A) :=
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  forall (a : A), m1 a -> m2 a.

Infix "\subset" := set_incl (at level 70, no associativity) : set_scope.

Notation "[ 'set' x : T | P ]" := (fun x : T => P)
  (at level 0, x at level 99, only parsing) : set_scope.
Notation "[ 'set' x | P ]" := [set x : _ | P]
  (at level 0, x, P at level 99, format "[ 'set'  x  |  P ]", only parsing) : set_scope.

Definition set0 {T} := [set _ : T | False].

Definition setT {T} := [set _ : T | True].

Notation "[ 'set' : T ]" := (@setT T)
  (at level 0, format "[ 'set' :  T ]") : set_scope.

Section setOpsDef.

Context {T U : Type}.
Implicit Types (a x : T) (A B : set T).

Definition set1 a := eq a.

Definition setU A B := [set x | x \in A \/ x \in B].

Definition setI A B := [set x | x \in A /\ x \in B].

Definition codom (f : T -> U) := [set y | exists x, f x = y].

Definition bigcup A (F : T -> set U) := [set x | exists i, i \in A /\ x \in F i].

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Definition bigcap (A : set T) (F : T -> set U) :=
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  [set x | forall (i : T), i \in A -> x \in F i].

End setOpsDef.

Definition imset {T U} (f : T -> U) A := bigcup A (fun x => set1 (f x)).

Definition setX T U (A : set T) (B : set U) := [set x | x.1 \in A /\ x.2 \in B].

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Definition imset2 T U V (f : T -> U -> V) A1 A2 :=
  imset (prod_curry f) (setX A1 A2).

Definition codom2 T U V (f : T -> U -> V) := codom (prod_curry f).

Notation "[ 'set' a ]" := (set1 a)
  (at level 0, a at level 99, format "[ 'set'  a ]") : set_scope.
Notation "[ 'set' a : T ]" := [set (a : T)]
  (at level 0, a at level 99, format "[ 'set'  a   :  T ]") : set_scope.

Notation "A :|: B" := (setU A B) (at level 52, left associativity) : set_scope.
Notation "a |: A" := ([set a] :|: A) (at level 52, left associativity) : set_scope.

Notation "A :&: B" := (setI A B) (at level 48, left associativity) : set_scope.

Notation "f @: A" := (imset f A) (at level 24) : set_scope.

Notation "f @2: ( A , B )" := (imset2 f A B)
  (at level 24, format "f  @2:  ( A ,  B )") : set_scope.

Notation "\bigcup_ i F" := (bigcup setT (fun i => F))
  (at level 41, F at level 41, i at level 0,
           format "'[' \bigcup_ i '/  '  F ']'") : set_scope.
Notation "\bigcup_ ( i : t ) F" := (bigcup (@setT t) (fun i => F))
  (at level 41, F at level 41, i at level 50,
           format "'[' \bigcup_ ( i   :  t ) '/  '  F ']'", only parsing) : set_scope.
Notation "\bigcup_ ( i 'in' A ) F" := (bigcup A (fun i => F))
  (at level 41, F at level 41, i, A at level 50,
           format "'[' \bigcup_ ( i  'in'  A ) '/  '  F ']'") : set_scope.

Notation "\bigcap_ ( i 'in' A ) F" := (bigcap A (fun i => F))
  (at level 41, F at level 41, i, A at level 50,
           format "'[' \bigcap_ ( i  'in'  A ) '/  '  F ']'") : set_scope.

Definition lift {T} (S : set T) : set (option T) :=
  Some @: S :|: [set None].

Lemma subset_eqP T (A B : set T) : (A <--> B) <-> (A \subset B /\ B \subset A).
Proof.
(* Goal: and (A x) (@set_incl T (@seq_In T s) A) *)
split; first by move=> eqAB; split=> a; rewrite (eqAB a).
(* Goal: @set_eq A (@seq_In A (@cons A x l)) (@setU A (@set1 A x) (@seq_In A l)) *)
by case=> subAB subBA a; split; [apply: subAB | apply:subBA].
Qed.

Lemma subset_trans T (A1 A2 A3 : set T) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  A1 \subset A2 ->
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  A2 \subset A3 ->
  A1 \subset A3.
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  now firstorder.
Qed.

Lemma subset_refl T (A : set T) : A \subset A.
Proof.
(* Goal: @set_eq A (@seq_In A (@cons A x l)) (@setU A (@set1 A x) (@seq_In A l)) *)
    by rewrite /set_incl.
Qed.

Lemma subset_singl : 
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  forall {T} (x y : T), [set x] \subset [set y] <-> y = x. 
Proof.
(* Goal: forall _ : @set_eq A s2 s2', @set_eq A (@setI A s1 s2) (@setI A s1 s2') *)
  intros. split; intros H; subst; auto.  
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  - apply H; reflexivity.
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  - apply subset_refl.
Qed.

Lemma subset_respects_set_eq_l :
  forall (T : Type) (s1 s2 s3 : set T),
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
    s1 <--> s3 -> s3 \subset s2 -> s1 \subset s2.
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  now firstorder.
Qed.

Lemma subset_respects_set_eq_r :
  forall (T : Type) (s1 s2 s3 : set T),
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
    s3 <--> s2 -> s1 \subset s2 -> s1 \subset s3.
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  now firstorder.
Qed.

Lemma subset_respects_set_eq :
  forall {T : Type} {s1 s2 s1' s2' : set T},
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
    s1 <--> s1' ->
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
    s2 <--> s2' ->
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
    s1' \subset s2' ->
    s1 \subset s2.
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma imsetT T U (f : T -> U) : f @: setT <--> codom f.
Proof.
(* Goal: and (A x) (@set_incl T (@seq_In T s) A) *)
  move=> y; split; first by case=> x [_ fx]; exists x.
(* Goal: @set_eq A (@seq_In A (@cons A x l)) (@setU A (@set1 A x) (@seq_In A l)) *)
    by case=> x fx; exists x.
Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma imset_id T (A : set T) : id @: A <--> A.
Proof.
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
    by move=> t; split=> [[x [Ax <-]]|At] //; exists t.
Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma imset_incl {T U} (A B : set T) (f : T -> U):
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  A \subset B -> 
  f @: A \subset f @: B.
Proof.
(* Goal: forall _ : @setT U a, @bigcap T U (@set0 T) (fun x : T => F x) a *)
  move => H u [x [H1 H2]]. eexists; split; eauto.
Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma imset_eq {T U} (A B : set T) (f : T -> U):
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  A <--> B -> 
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  f @: A <--> f @: B.
Proof.
(* Goal: forall _ : @setT U a, @bigcap T U (@set0 T) (fun x : T => F x) a *)
  move => H u. split; apply imset_incl => t Ht; by apply H.
Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma imset_in a b x (f : a -> b) (A : set a) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  x \in A -> f x \in (f @: A).
Proof.
(* Goal: forall _ : @set_eq A s2 s2', @set_eq A (@setI A s1 s2) (@setI A s1 s2') *)
  intros. unfold imset. exists x. split; by [].
Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma imset_id_ext T (A : set T) f : (forall x, f x = x) -> f @: A <--> A.
Proof.
  rewrite /imset /bigcup => H x. split.
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  - move => [y [H1 H2]]. rewrite H in H2. inversion H2. subst. assumption.
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  - move => H1. eexists. split. eassumption. by rewrite H.
Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma imset_eq_ext a b (f g : a -> b) (A : set a) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  (forall x, f x = g x) ->
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  f @: A <--> g @: A.
Proof.
(* Goal: @set_incl (option B) (@imset B (option B) (@Some B) (@setU B s1 s2)) (@bigcup A (option B) (@setI A (@seq_In A (@cons A l ls)) s3) (fun x : A => f x)) *)
  rewrite /imset /bigcup /set1. move => H x.
  split => [[i [H1 H2]] | [i [H1 H2]]]; eexists; split;
(* Goal: f y a *)
           try eassumption. congruence. congruence.
Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma coverE T (A : set T) : \bigcup_(x in A) [set x] <--> A.
Proof. exact: imset_id. Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma setXT T U : setX [set: T] [set: U] <--> [set: T * U].
Proof. by case. Qed.

Instance set_incl_Proper T U :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  Proper (@eq (T -> U) ==> set_incl ==> set_incl) imset.
Proof.
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
by move=> f ? <- A B subAB y [x [Ax fx]]; exists x; split=> //; apply: subAB.
Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Instance set_eq_Proper T U : Proper (@eq (T -> U) ==> set_eq ==> set_eq) imset.
Proof.
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
by move=> f ? <- A B /subset_eqP[subAB subBA] y; split; apply: set_incl_Proper.
Qed.

Lemma sub0set T (A : set T) : set0 \subset A.
Proof. by []. Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma bigcup_set0 T U (F : T -> set U) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  \bigcup_(x in set0) F x <--> set0.
Proof. by move=> t; split=> // [[? []]]. Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma imset0 T U (f : T -> U) : f @: set0 <--> set0.
Proof. exact: bigcup_set0. Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma bigcup_set1 T U (F : T -> set U) y :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  \bigcup_(x in [set y]) F x <--> F y.
Proof. by move=> t; split=> [[y' [<-]] | Fyt] //; exists y. Qed.

Lemma bigcup_setU_l:
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  forall (U T : Type) (s1 s2 : set U) (f : U -> set T),
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  \bigcup_(i in (s1 :|: s2)) f i <-->
  \bigcup_(i in s1) f i :|: \bigcup_(i in s2) f i.
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma bigcup_const A B (P : set B) : inhabited A -> (\bigcup_(_ : A) P) <--> P.
Proof. by case=> a x; split=> [[?] []|Px] //; exists a. Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma bigcup_const_2 A (x :A) B (P : set B) : (\bigcup_(_ in [set x]) P) <--> P.
Proof. by split=> [[?] []|Px] //; exists x; split => //=. Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma bigcupC T U V A B (F : T -> U -> set V) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  \bigcup_(i in A) \bigcup_(j in B) F i j <-->
  \bigcup_(j in B) \bigcup_(i in A) F i j.
Proof.
  wlog suff: T U A B F / \bigcup_(i in A) \bigcup_(j in B) F i j \subset
   \bigcup_(j in B) \bigcup_(i in A) F i j.
(* Goal: @set_eq A (@seq_In A (@cons A x l)) (@setU A (@set1 A x) (@seq_In A l)) *)
  by move=> sub; apply/subset_eqP; split; apply: sub.
(* Goal: @set_eq A (@seq_In A (@cons A x l)) (@setU A (@set1 A x) (@seq_In A l)) *)
    by move=> x [i [Ai [j [Bj ?]]]]; exists j; split=> //; exists i.
Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma incl_bigcupr T U A (F : T -> set U) G : (forall x, F x \subset G x) ->
  \bigcup_(x in A) F x \subset \bigcup_(x in A) G x.
Proof.
(* Goal: @set_eq A (@seq_In A (@cons A x l)) (@setU A (@set1 A x) (@seq_In A l)) *)
  by move=> subFG t [x [Ax Fxt]]; exists x; split=> //; apply: subFG.
Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma eq_bigcupr T U A (F : T -> set U) G : (forall x, F x <--> G x) ->
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  \bigcup_(x in A) F x <--> \bigcup_(x in A) G x.
Proof.
(* Goal: @set_eq A (@seq_In A (@cons A x l)) (@setU A (@set1 A x) (@seq_In A l)) *)
  by move=> eq_FG t; split; apply: incl_bigcupr => {t} x t; rewrite (eq_FG x t).
Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma incl_bigcupl T U A B (F : T -> set U) : A \subset B ->
  \bigcup_(x in A) F x \subset \bigcup_(x in B) F x.
Proof.
(* Goal: @set_eq A (@seq_In A (@cons A x l)) (@setU A (@set1 A x) (@seq_In A l)) *)
    by move=> subAB t [x [Ax Fxt]]; exists x; split=> //; apply: subAB.
Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma eq_bigcupl T U A B (F : T -> set U) : A <--> B ->
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  \bigcup_(x in A) F x <--> \bigcup_(x in B) F x.
Proof.
(* Goal: @set_eq A (@seq_In A (@cons A x l)) (@setU A (@set1 A x) (@seq_In A l)) *)
  by move=> /subset_eqP[? ?]; split; apply: incl_bigcupl.
Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma incl_bigcup a b (x:a) (A : set a) (f:a->set b) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  x \in A -> 
  f x \subset \bigcup_(x in A) f x.
Proof.
(* Goal: @set_incl (option B) (@imset B (option B) (@Some B) (@setU B s1 s2)) (@bigcup A (option B) (@setI A (@seq_In A (@cons A l ls)) s3) (fun x : A => f x)) *)
  rewrite /set_incl /bigcup. by eauto 3.
Qed.


Arguments eq_bigcupl [T U A] B F _ _.

Global Instance eq_bigcup T U : Proper (set_eq ==> pointwise_relation T (@set_eq U) ==> set_eq) bigcup.
Proof.
  move=> A B eqAB F G eqFG a; apply: (@set_eq_trans _ (\bigcup_(i in A) G i)).
(* Goal: @set_eq U (@imset T U f (@set0 T)) (@set0 U) *)
  exact: eq_bigcupr.
(* Goal: @set_eq U (@imset T U f (@set0 T)) (@set0 U) *)
  exact: eq_bigcupl.
Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma bigcup_flatten T U V A (F : T -> set U) (G : U -> set V) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  \bigcup_(x in \bigcup_(y in A) F y) G x <-->
  \bigcup_(y in A) \bigcup_(x in F y) G x.
Proof.
(* Goal: @set_eq V (@bigcup U V (@bigcup T U A (fun y : T => F y)) (fun x : U => G x)) (@bigcup T V A (fun y : T => @bigcup U V (F y) (fun x : U => G x))) *)
move=> t; split=> [[x [[y [Ay Fyx]] Gxt]] | [y [Ay [x [Fyx Gxt]]]]].
(* Goal: @bigcup a b A (fun x : a => @set1 b (f x)) (f x) *)
  by exists y; split=> //; exists x.
(* Goal: @set_eq A (@seq_In A (@cons A x l)) (@setU A (@set1 A x) (@seq_In A l)) *)
by exists x; split=> //; exists y.
Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma codom_apply {A B : Type} {f : A -> B} {x : A} : f x \in codom f.
Proof. eexists; eauto. Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma codomE T U (f : T -> U) : codom f <--> \bigcup_x [set f x].
Proof. by move=> y; split=> [[x fx]|[x [_ fx]]]; exists x. Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma codom_id T : codom id <--> [set: T].
Proof. by move=> x; split=> // _; exists x. Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma codom_const A B (x : B) : inhabited A ->
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  codom (fun _ : A => x) <--> [set x].
Proof. by move=> ?; rewrite codomE bigcup_const. Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma imset_comp T U V (f : U -> T) (g : V -> U) A :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  (f \o g) @: A <--> f @: (g @: A).
Proof.
(* Goal: @set_eq A (@seq_In A (@cons A x l)) (@setU A (@set1 A x) (@seq_In A l)) *)
by rewrite /imset bigcup_flatten; apply: eq_bigcupr => x; rewrite bigcup_set1.
Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma codom_comp T U V (f : U -> T) (g : V -> U) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  codom (f \o g) <--> f @: (codom g).
Proof. by rewrite -imsetT imset_comp imsetT. Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma curry_imset2l T U V (f : T -> U -> V) A1 A2 :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  f @2: (A1, A2) <--> \bigcup_(x1 in A1) f x1 @: A2.
Proof.
(* Goal: @setI (option A) (fun u : option A => is_true (@isSome A u)) s (@Some A y) *)
move=> a; split.
(* Goal: @set_eq A (@seq_In A (@cons A x l)) (@setU A (@set1 A x) (@seq_In A l)) *)
  by case=> [[x1 x2] [[/= Ax1 Ax2] fx]]; exists x1; split=> //; exists x2.
(* Goal: @set_eq A (@seq_In A (@cons A x l)) (@setU A (@set1 A x) (@seq_In A l)) *)
by case=> [x1 [Ax1 [x2 [Ax2 fx]]]]; exists (x1,x2).
Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma curry_imset2r T U V (f : T -> U -> V) A1 A2 :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  f @2: (A1, A2) <--> \bigcup_(x2 in A2) f^~ x2 @: A1.
Proof. by rewrite curry_imset2l bigcupC. Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma curry_codom2l T U V (f : T -> U -> V) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  codom (prod_curry f) <--> \bigcup_x1 codom (f x1).
Proof.
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
rewrite -imsetT -setXT -/(imset2 f _ _) curry_imset2l.
(* Goal: @set_eq A (@seq_In A (@cons A x l)) (@setU A (@set1 A x) (@seq_In A l)) *)
by apply: eq_bigcupr => x; rewrite imsetT.
Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma imset_bigcup T U V (f : U -> V) A (F : T -> set U) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  (f @: \bigcup_(x in A) (F x)) <--> \bigcup_(x in A) f @: F x.
Proof. by rewrite /imset bigcup_flatten. Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma bigcup_imset T U V (f : T -> U) A (F : U -> set V) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  \bigcup_(y in f @: A) (F y) <--> \bigcup_(x in A) F (f x).
Proof.
(* Goal: @set_eq A (@seq_In A (@cons A x l)) (@setU A (@set1 A x) (@seq_In A l)) *)
by rewrite bigcup_flatten; apply: eq_bigcupr => x; rewrite bigcup_set1.
Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma bigcup_codom T U V (f : T -> U) (F : U -> set V) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  \bigcup_(y in codom f) (F y) <--> \bigcup_x F (f x).
Proof. by rewrite -imsetT bigcup_imset. Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Coercion seq_In T : seq T -> set T := fun s x => List.In x s.
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Coercion list_In T : list T -> set T := fun s x => List.In x s.

Lemma subnilset T (A : set T) : [::] \subset A.
Proof. by []. Qed.

Lemma subconsset T (A : set T) x s :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  x :: s \subset A <-> x \in A /\ s \subset A.
Proof.
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
split=> [sub|[Ax sub] a [<-|?]] //; last by apply: sub.
(* Goal: and (A x) (@set_incl T (@seq_In T s) A) *)
split=> [|a sa]; apply: sub; first by left.
(* Goal: @set_eq A (@seq_In A (@cons A x l)) (@setU A (@set1 A x) (@seq_In A l)) *)
by right.
Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma reindex_bigcup I J K (h : J -> I) (F : I -> set K) A B :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  h @: B <--> A ->
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  \bigcup_(x in A) F x <--> \bigcup_(y in B) F (h y).
Proof.
(* Goal: @setI (option A) (fun u : option A => is_true (@isSome A u)) s (@Some A y) *)
move=> surj t; split.
(* Goal: forall _ : @bigcup I K A (fun x : I => F x) t, @bigcup J K B (fun y : J => F (h y)) t *)
(* Goal: forall _ : @bigcup J K B (fun y : J => F (h y)) t, @bigcup I K A (fun x : I => F x) t *)
  case=> x [Ax Fxt]; case: (surj x) => [?].
(* Goal: @set_eq A (@seq_In A (@cons A x l)) (@setU A (@set1 A x) (@seq_In A l)) *)
  by case=> // y [By eq_hyx]; exists y; rewrite eq_hyx.
(* Goal: forall _ : @bigcup J K B (fun y : J => F (h y)) t, @bigcup I K A (fun x : I => F x) t *)
case=> y [By Fhyt]; exists (h y); split=> //.
(* Goal: @set_eq A (@seq_In A (@cons A x l)) (@setU A (@set1 A x) (@seq_In A l)) *)
by case: (surj (h y)) => Ahy _; apply: Ahy; exists y.
Qed.
Arguments reindex_bigcup [I J K] h [F A] B _ _.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma bigcup_pointwise_incl A B (s : set A) (t : A -> set B) (u : set B) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  (forall x, x \in s -> t x \subset u) ->
  \bigcup_(x in s) t x \subset u.
Proof.
(* Goal: forall _ : forall (x : A) (_ : s x), @set_incl B (t x) u, @set_incl B (@bigcup A B s (fun x : A => t x)) u *)
  intros H b [x []]; eapply H; eauto.
Qed.

Instance proper_set_incl A :
  Morphisms.Proper (set_eq ==> set_eq ==> Basics.impl) (@set_incl A).
Proof. firstorder. Qed.

(** Lemmas about [setU] and [setI] *)

Instance eq_setU U : Proper (set_eq ==> set_eq ==> set_eq) (@setU U).
Proof.
(* Goal: forall _ : @setT U a, @bigcap T U (@set0 T) (fun x : T => F x) a *)
  move=> A B eqAB F G eqFG a.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  split; by move => [H1 | H2]; firstorder.
Qed.

Instance eq_setI U : Proper (set_eq ==> set_eq ==> set_eq) (@setI U).
Proof.
(* Goal: forall _ : @setT U a, @bigcap T U (@set0 T) (fun x : T => F x) a *)
  move=> A B eqAB F G eqFG a.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  by split; move => [H1 H2]; firstorder.
Qed.

Lemma setI_comm {U} (s1 s2 : set U) : 
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
   s1 :&: s2 <--> s2 :&: s1.
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.

Lemma setU_comm {U} (s1 s2 : set U) : 
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
   s1 :|: s2 <--> s2 :|: s1.
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.

Lemma setI_set0_abs {U} (s : set U) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  (s :&: set0) <--> set0.
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.

Lemma setU_set0_neut {U} (s : set U) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  (s :|: set0) <--> s.
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.

Lemma setU_set0_neut_eq {A} (s s1 : set A) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  s1 <--> set0 ->
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  s <--> s :|: s1.
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.

Lemma setU_set0_l {A} (s1 s2 s3 : set A) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  s1 <--> set0 ->
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  s2 <--> s3 ->
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  (s1 :|: s2) <--> s3. 
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.

Lemma setU_set0_r {A} (s1 s2 s3 : set A) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  s1 <--> set0 ->
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  s3 <--> s2 ->
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  s3 <--> (s1 :|: s2). 
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.

Lemma setI_setT_neut {U} (s : set U) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  (s :&: setT) <--> s.
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.

Lemma setU_setT_abs {U} (s : set U) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  (s :|: setT) <--> setT.
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.

Lemma setU_set_eq_compat {T} (s1 s2 s1' s2' : set T) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  s1 <--> s1' ->
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  s2 <--> s2' ->
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  s1 :|: s2 <--> s1' :|: s2'.
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  by firstorder.
Qed.

Lemma setU_set_subset_compat :
  forall (T : Type) (s1 s2 s1' s2' : set T),
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
    s1 \subset s1' -> s2 \subset s2' -> s1 :|: s2 \subset s1' :|: s2'.
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  now firstorder.
Qed.

Lemma setU_set_incl_r :
  forall (T : Type) (s1 s2 s2' : set T),
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
    s1 \subset s2' -> s1 \subset s2 :|: s2'.
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  now firstorder.
Qed.

Lemma setU_assoc {U} (s1 s2 s3 : set U) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  (s1 :|: (s2 :|: s3)) <--> ((s1 :|: s2) :|: s3).
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.

Lemma setI_assoc {U} (s1 s2 s3 : set U) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  (s1 :&: (s2 :&: s3)) <--> ((s1 :&: s2) :&: s3).
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma setI_impl_l {T} (s1 s2 : set T) : s1 \subset s2 -> s1 :&: s2 <--> s1.
Proof.      
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.      

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma setI_impl_r {T} (s1 s2 : set T) : s2 \subset s1 -> s1 :&: s2 <--> s2.
Proof.      
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.      

Lemma setI_set0 {U} (s1 s2 : set U) : 
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  (forall x, s1 x -> ~ s2 x) ->
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  (s1 :&: s2) <--> set0.
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  intros; split; firstorder. 
Qed.

Lemma setI_subset_compat {U} (s1 s2 s1' s2' : set U) : 
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  s1 \subset s1' ->
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  s2 \subset s2' ->
  (s1 :&: s2) \subset (s1' :&: s2').
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.

Lemma setU_subset_r {U} (s1 s2 s3 : set U) : 
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  s1 \subset s3 ->
  s1 \subset (s2 :|: s3).
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.

Lemma setU_subset_l {U} (s1 s2 s3 : set U) : 
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  s1 \subset s2 ->
  s1 \subset (s2 :|: s3).
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.

Lemma setI_setU_distr {U} (s1 s2 s3 : set U) : 
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  ((s1 :|: s2) :&: s3) <--> ((s1 :&: s3) :|: (s2 :&: s3)).
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.

(** Lemmas about [bigcap] *)

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma bigcap_set0 (T U : Type) (F : T -> set U) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  \bigcap_(x in set0) F x <--> setT.
Proof.
(* Goal: @setI (option A) (fun u : option A => is_true (@isSome A u)) s (@Some A y) *)
  split.
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  - move => _. constructor.
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  - move => _ x H. inversion H.
Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma incl_bigcapl T U A B (F : T -> set U) : B \subset A ->
  \bigcap_(x in A) F x \subset \bigcap_(x in B) F x.
Proof.
(* Goal: @set_eq A (@seq_In A (@cons A x l)) (@setU A (@set1 A x) (@seq_In A l)) *)
  by move => Hsub t Hcap x HB; eauto.
Qed.


(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma eq_bigcapr (T U : Type) (A : set T) (F G : T -> set U) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  (forall x : T, F x <--> G x) ->
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  \bigcap_(x in A) F x <--> \bigcap_(x in A) G x.
Proof.
(* Goal: @set_eq A (@seq_In A (@cons A x l)) (@setU A (@set1 A x) (@seq_In A l)) *)
  by move => H a; split; move => Ha b Hb; eapply H; eauto.
Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma eq_bigcapl T U A B (F : T -> set U) : A <--> B ->
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  \bigcap_(x in A) F x <--> \bigcap_(x in B) F x.
Proof.
(* Goal: @set_eq A (@seq_In A (@cons A x l)) (@setU A (@set1 A x) (@seq_In A l)) *)
  by move => H a; split; move => Ha b Hb; eapply Ha; eapply H; eauto.
Qed.


Instance eq_bigcap T U : Proper (set_eq ==> pointwise_relation T (@set_eq U) ==> set_eq) bigcap.
Proof.
(* Goal: forall _ : @setT U a, @bigcap T U (@set0 T) (fun x : T => F x) a *)
  move=> A B eqAB F G eqFG a. apply: (@set_eq_trans _ (\bigcap_(i in A) G i)).
(* Goal: @set_eq U (@imset T U f (@set0 T)) (@set0 U) *)
  exact: eq_bigcapr.
(* Goal: @set_eq U (@imset T U f (@set0 T)) (@set0 U) *)
  exact: eq_bigcapl.
Qed.


Lemma eq_bigcup' :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  forall (T U : Type) (A B : set T) (F G : T -> set U),
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
    A <--> B ->
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
    (forall x, F x <--> G x) ->
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
    \bigcup_(x in A) F x <--> \bigcup_(x in B) G x.
Proof.
(* Goal: forall _ : @set_eq A s2 s2', @set_eq A (@setI A s1 s2) (@setI A s1 s2') *)
  intros.
(* Goal: @set_eq U (@bigcup T U A (fun x : T => F x)) (@bigcup T U B (fun x : T => G x)) *)
  eapply eq_bigcup; eauto.
Qed.

Lemma incl_bigcup_compat :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  forall (T U : Type) (A B : set T) (F G : T -> set U),
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
    A \subset B ->
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
    (forall x : T, F x \subset G x) ->
    \bigcup_(x in A) F x \subset \bigcup_(x in B) G x.
Proof. 
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  now firstorder. 
Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma bigcap_setI_l {U T} (s1 s2 : set U) (f : U -> set T) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  bigcap (s1 :|: s2) f <-->
  bigcap s1 f :&: bigcap s2 f.
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma bigcap_setU_l {U T} (s1 s2 : set U) (f : U -> set T) :
  bigcap s1 f \subset bigcap (s1 :&: s2) f.
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma bigcap_set1 {U T} (x : U) (f : U -> set T) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  bigcap [set x] f <--> f x.
Proof.
(* Goal: @set_eq T (@bigcap U T (@set1 U x) f) (f x) *)
  split; move => H.
(* Goal: @imset A (option A) (@Some A) s' (@Some A x) *)
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  eapply H. reflexivity.
(* Goal: f y a *)
  intros y Hy. inversion Hy. subst.
(* Goal: f y a *)
  assumption.
Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma bigcup_set0_r (T U : Type) (s : set T) (F : T -> set U) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  (forall x, F x <--> set0) ->
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  \bigcup_(x in s) F x <--> set0.
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma bigcup_set0_l_eq (T U : Type) (s : set T) (F : T -> set U) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  s <--> set0 ->
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  \bigcup_(x in s) F x <--> set0.
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.

(** Lemmas about lists *)
Lemma nil_set_eq {A : Type} :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  [::] <--> (@set0 A).
Proof.
(* Goal: @set_eq A (@seq_In A (@nil A)) (@set0 A) *)
  split; move => H; eauto.
Qed.

Lemma cons_set_eq {A} (x : A) l :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  (x :: l) <--> [set x] :|: l.
Proof. by []. Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma singl_set_eq: forall (A : Type) (x : A), [ x ] <--> [ set x ].
Proof.
(* Goal: forall (A : Type) (x : A), @set_eq A (@seq_In A (@cons A x (@nil A))) (@set1 A x) *)
  intros A x x'; split; intros H.
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  - inv H. reflexivity. now inv H0.
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  - inv H. now constructor.
Qed.

Lemma incl_subset {A : Type} (l1 l2 : seq A) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  incl l1 l2 -> l1 \subset l2.
Proof.
(* Goal: forall _ : @incl A l1 l2, @set_incl A (@seq_In A l1) (@seq_In A l2) *)
  intros Hi x; eapply Hi.
Qed.

Lemma incl_hd_same {A : Type} (a : A) (l1 l2 : seq A) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  incl l1 l2 -> incl (a :: l1) (a :: l2).
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  intros Hin. firstorder.
Qed.
     
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma setI_bigcup_assoc {A B} (s1 : set B) (s2 : set A) (s3 : A -> set B) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  s1 :&: (\bigcup_(x in s2) s3 x) <--> \bigcup_(x in s2) (s1 :&: (s3 x)).
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.

Lemma cons_subset {A : Type} (x : A) (l : seq A) (P : set A) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  P x ->
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  l \subset P ->
  (x :: l) \subset P.
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  intros Px Pl x' Hin. inv Hin; firstorder.
Qed.

Lemma nil_subset {A : Type} (P : set A) :
  [] \subset P.
Proof.
(* Goal: @setU (option A) s2 (@setI (option A) (@set1 (option A) (@None A)) s2') (@Some A x) *)
  intros x H; inv H.
Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma imset_union_incl {U T : Type} (s1 s2 : set U) (f : U -> T) :
  f @: (s1 :|: s2) \subset (f @: s1) :|: (f @: s2).
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma imset_singl_incl {U T : Type} (x : U) (f : U -> T) :
  f @: [set x] \subset [set (f x)].
Proof.
(* Goal: @set_incl T (@imset U T f (@set1 U x)) (@set1 T (f x)) *)
  intros y Hin. destruct Hin as [y' [Hin1 Hin2]].
(* Goal: @set_eq (option T) (@setU (option T) (@imset T (option T) (@Some T) (@bigcup U T (@setT U) (fun i : U => f i))) (@set1 (option T) (@None T))) (@setU (option T) (@imset T (option T) (@Some T) (@bigcup U T (@setT U) (fun x : U => f x))) (@set1 (option T) (@None T))) *)
  inv Hin1. inv Hin2. reflexivity.
Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma imset_set0_incl  {U T : Type} (f : U -> T) :
  f @: set0 \subset set0.
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.

Lemma set_eq_set_incl_r {U : Type} (s1 s2 : set U) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  s1 <--> s2 -> s2 \subset s1.
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.

Lemma set_eq_set_incl_l {U : Type} (s1 s2 : set U) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  s1 <--> s2 -> s1 \subset s2.
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.

Lemma rewrite_set_l {U : Type} (s1 s2 : set U) x :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  s1 x ->
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  s1 <--> s2 ->
  s2 x.
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.

Lemma rewrite_set_r {U : Type} (s1 s2 : set U) x :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  s2 x ->
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  s1 <--> s2 ->
  s1 x.
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.

Lemma imset_bigcup_incl_l :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  forall {T U V : Type} (f : U -> V) (A : set T) (F : T -> set U),
  f @: (\bigcup_(x in A) F x) \subset \bigcup_(x in A) f @: F x.
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma in_imset {U T} (f : U -> T) (S : set U) (x : T) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  (f @: S) x -> exists y, x = f y.
Proof.
(* Goal: forall _ : @imset U T f S x, @ex U (fun y : U => @eq T x (f y)) *)
  move => [y [H1 H2]]; eauto.
Qed.

Lemma union_lift_subset_compat {A} (s1 s2 : set (option A)) (s3 s4 : set A) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  s1 \subset lift s3 ->
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  s2 \subset lift s4 ->
  (s1 :|: s2) \subset lift (s3 :|: s4).
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.

Lemma lift_subset_pres_l {A} (s1 : set (option A)) (s2 s3 : set A) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  s1 \subset lift s2 ->
  s1 \subset lift (s2 :|: s3).
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.

Lemma lift_subset_pres_r {A} (s1 : set (option A)) (s2 s3 : set A) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  s1 \subset lift s3 ->
  s1 \subset lift (s2 :|: s3).
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.


Lemma set_incl_setI_l {A} (s1 s2 s3 : set A) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  s1 \subset s3 ->
  (s1 :&: s2) \subset s3.
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.

Lemma set_incl_setI_r {A} (s1 s2 s3 : set A) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  s2 \subset s3 ->
  (s1 :&: s2) \subset s3.
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.

Lemma set_incl_setU_l {A} (s1 s2 s3 : set A) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  s1 \subset s3 ->
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  s2 \subset s3 ->
  (s1 :|: s2) \subset s3.
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma bigcup_set_I_l {A B} (s1 s2 : set A) (s3 : set B) (f : A -> set B) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  \bigcup_(x in s1) (f x) \subset s3 ->
  \bigcup_(x in (s1 :&: s2)) (f x) \subset s3.
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma bigcup_set_U {A B} (s1 s2 : set A) (s3 : set B) (f : A -> set B) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  \bigcup_(x in s1) (f x) \subset s3 ->
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  \bigcup_(x in s2) (f x) \subset s3 ->
  \bigcup_(x in (s1 :|: s2)) (f x) \subset s3.
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma bigcup_set0_subset {A B} (s : set B) (f : A -> set B) :
  \bigcup_(x in set0) (f x) \subset s.
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma bigcup_cons_subset {A B} l (ls : seq A) (f : A -> set B) s :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  f l \subset s ->
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  \bigcup_(x in ls) (f x) \subset s ->
  \bigcup_(x in l :: ls) (f x) \subset s. 
Proof.
(* Goal: forall (_ : @set_incl B (f l) s) (_ : @set_incl B (@bigcup A B (@seq_In A ls) (fun x : A => f x)) s), @set_incl B (@bigcup A B (@seq_In A (@cons A l ls)) (fun x : A => f x)) s *)
  intros H1 H2 x [y [Hl Hr]].
(* Goal: s x *)
  inv Hl.
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  - eauto.
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  - eapply H2. eexists; split; eauto.
Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma bigcup_nil_subset {A B} (f : A -> set B) s :
  \bigcup_(x in []) (f x) \subset s. 
Proof.
(* Goal: @set_incl B (@bigcup A B (@seq_In A (@nil A)) (fun x : A => f x)) s *)
  intros x [y [H1 H2]]. inv H1.
Qed.

Lemma option_subset {A} (s1 : set (option A)) :
  s1 \subset (isSome :&: s1) :|: [set None]. 
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  intros [x |]; firstorder.
Qed.

Lemma setU_l_subset {U} (s1 s2 s3 : set U) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  s1 \subset s3 ->
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  s2 \subset s3 ->
  (s1 :|: s2) \subset s3.
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma bigcup_lift_lift_bigcup {T U} (s1 : set T) (f : T -> set U) :
  \bigcup_(x in s1) (lift (f x)) \subset lift (\bigcup_(x in s1) (f x)).
Proof.
(* Goal: @set_incl (option U) (@bigcup T (option U) s1 (fun x : T => @lift U (f x))) (@lift U (@bigcup T U s1 (fun x : T => f x))) *)
  intros x [y [H1 [[z [H2 H3]] | H2]]].
(* Goal: @imset A (option A) (@Some A) s' (@Some A y) *)
  + inv H3. left; eexists; split; eauto.
(* Goal: @imset A (option A) (@Some A) s' (@Some A y) *)
    eexists; split; eauto.
(* Goal: @lift U (@bigcup T U s1 (fun x : T => f x)) x *)
  + inv H2; now right. 
Qed.

Lemma lift_subset_compat {U} (s1 s2 : set U) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  s1 \subset s2 ->
  lift s1 \subset lift s2.
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.

Lemma lift_set_eq_compat {U} (s1 s2 : set U) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  s1 <--> s2 ->
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  lift s1 <--> lift s2.
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.

Lemma bigcup_setU_r:
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  forall (U T : Type) (s : set U) (f g : U -> set T),
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
    \bigcup_(i in s) (f i :|: g i) <-->
    \bigcup_(i in s) f i :|: \bigcup_(i in s) g i.
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.

Lemma lift_bigcup_comm :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  forall (U T : Type) (s : set U) (f : U -> set T),
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
    inhabited U ->
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
    lift (\bigcup_(i in [set : U]) (f i)) <-->
    \bigcup_(i in [set : U]) (lift (f i)).
Proof.
(* Goal: forall (U T : Type) (_ : set U) (f : forall _ : U, set T) (_ : inhabited U), @set_eq (option T) (@lift T (@bigcup U T (@setT U) (fun i : U => f i))) (@bigcup U (option T) (@setT U) (fun i : U => @lift T (f i))) *)
  intros U T s f Hin. unfold lift.
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  rewrite !bigcup_setU_r -!imset_bigcup.
(* Goal: is_true (@isSome A (@Some A x)) *)
  rewrite bigcup_const; eauto.
(* Goal: @set_eq (option T) (@setU (option T) (@imset T (option T) (@Some T) (@bigcup U T (@setT U) (fun i : U => f i))) (@set1 (option T) (@None T))) (@setU (option T) (@imset T (option T) (@Some T) (@bigcup U T (@setT U) (fun x : U => f x))) (@set1 (option T) (@None T))) *)
  reflexivity.
Qed.

Lemma bigcap_setU_distr:
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  forall (U T : Type) (s1 s2 : set U) (f : U -> set T),
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
    \bigcap_(i in s1) f i :&: \bigcap_(i in s2) f i <--> \bigcap_(i in s1 :|: s2) f i.
Proof.
(* Goal: forall _ : @set_eq A s2 s2', @set_eq A (@setI A s1 s2) (@setI A s1 s2') *)
  intros. split.
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  - intros [ H1 H2 ] x [ H3 | H3 ]; eauto.
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  - intros H. split; intros x H3; eapply H.
(* Goal: @setU U s1 s2 x *)
(* Goal: @setU U s1 s2 x *)
    now left. now right.
Qed.

Lemma setI_set_incl :
  forall (A : Type) (s1 s2 s3 : set A),
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
    s1 \subset s2 ->
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
    s1 \subset s3 ->
    s1 \subset s2 :&: s3.
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.

Lemma imset_isSome {A} (s : set A) :
  Some @: s \subset isSome.
Proof.
(* Goal: @setU (option A) s2 (@setI (option A) (@set1 (option A) (@None A)) s2') (@Some A x) *)
  intros y [x [Sx H]]. inv H. eauto.
Qed.

Lemma bigcup_cons_subset_r :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  forall (A B : Type) (l : A) (ls : seq A) (f : A -> set B) (s1 s2 : set B),
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
    s1 \subset f l ->
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
    s2 \subset \bigcup_(x in ls) f x ->
    s1 :|: s2 \subset \bigcup_(x in (l :: ls)) f x.
Proof.
(* Goal: forall (A B : Type) (l : A) (ls : list A) (f : forall _ : A, set B) (s1 s2 : set B) (_ : @set_incl B s1 (f l)) (_ : @set_incl B s2 (@bigcup A B (@seq_In A ls) (fun x : A => f x))), @set_incl B (@setU B s1 s2) (@bigcup A B (@seq_In A (@cons A l ls)) (fun x : A => f x)) *)
  intros A B l ls f s1 s2 H1 H2.
(* Goal: @set_incl (option B) (@setU (option B) (@imset B (option B) (@Some B) s1) (@imset B (option B) (@Some B) s2)) (@bigcup A (option B) (@setI A (@seq_In A (@cons A l ls)) s3) (fun x : A => f x)) *)
  apply setU_l_subset.
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  - rewrite bigcup_setU_l bigcup_set1.
(* Goal: f y a *)
    eapply setU_subset_l. eassumption.
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  - rewrite bigcup_setU_l bigcup_set1.
(* Goal: f y a *)
    eapply setU_subset_r. eassumption.
Qed.

Lemma bigcup_setI_cons_subset_r :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  forall (A B : Type) (l : A) (ls : seq A) (f : A -> set B) (s1 s2 : set B) (s3 : set A),
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
    s3 l ->
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
    s1 \subset f l ->
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
    s2 \subset \bigcup_(x in ls :&: s3) f x ->
    s1 :|: s2 \subset \bigcup_(x in (l :: ls) :&: s3) f x.
Proof.
(* Goal: forall (A B : Type) (l : A) (ls : list A) (f : forall _ : A, set (option B)) (s1 s2 : set B) (s3 : set A) (_ : s3 l) (_ : @set_incl (option B) (@imset B (option B) (@Some B) s1) (f l)) (_ : @set_incl (option B) (@imset B (option B) (@Some B) s2) (@bigcup A (option B) (@setI A (@seq_In A ls) s3) (fun x : A => f x))), @set_incl (option B) (@imset B (option B) (@Some B) (@setU B s1 s2)) (@bigcup A (option B) (@setI A (@seq_In A (@cons A l ls)) s3) (fun x : A => f x)) *)
  intros A B l ls f s1 s2 s3 H1 H2 H3.
(* Goal: @set_incl (option B) (@setU (option B) (@imset B (option B) (@Some B) s1) (@imset B (option B) (@Some B) s2)) (@bigcup A (option B) (@setI A (@seq_In A (@cons A l ls)) s3) (fun x : A => f x)) *)
  apply setU_l_subset.
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  - intros x Hs1. eexists l; split; eauto.
(* Goal: is_true (@isSome A (@Some A x)) *)
    split; eauto. left; eauto.
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  - intros x Hs1. eapply H3 in Hs1.
(* Goal: @bigcup A (option B) (@setI A (@seq_In A (@cons A l ls)) s3) (fun x : A => f x) x *)
    edestruct Hs1 as [x' [[Hs3 Hls] Hin]].
(* Goal: is_true (@isSome A (@Some A x)) *)
    eexists x'; split; eauto. split; eauto.
(* Goal: is_true (@isSome A (@Some A x)) *)
    right; eauto.
Qed.

Lemma imset_union_set_eq:
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  forall (U T : Type) (s1 s2 : set U) (f : U -> T),
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
    f @: (s1 :|: s2) <--> f @: s1 :|: f @: s2.
Proof.
(* Goal: forall (U T : Type) (s1 s2 : set U) (f : forall _ : U, T), @set_eq T (@imset U T f (@setU U s1 s2)) (@setU T (@imset U T f s1) (@imset U T f s2)) *)
  intros U T s1 s2 f.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.

Lemma imset_bigcup_setI_cons_subset_r :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  forall (A B : Type) (l : A) (ls : seq A) (f : A -> set (option B))
    (s1 s2 : set B) (s3 : set A),
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
    s3 l ->
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
    Some @: s1 \subset f l ->
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
    Some @: s2 \subset \bigcup_(x in ls :&: s3) f x ->
    Some @: (s1 :|: s2) \subset \bigcup_(x in (l :: ls) :&: s3) f x.
Proof.
(* Goal: forall (A B : Type) (l : A) (ls : list A) (f : forall _ : A, set (option B)) (s1 s2 : set B) (s3 : set A) (_ : s3 l) (_ : @set_incl (option B) (@imset B (option B) (@Some B) s1) (f l)) (_ : @set_incl (option B) (@imset B (option B) (@Some B) s2) (@bigcup A (option B) (@setI A (@seq_In A ls) s3) (fun x : A => f x))), @set_incl (option B) (@imset B (option B) (@Some B) (@setU B s1 s2)) (@bigcup A (option B) (@setI A (@seq_In A (@cons A l ls)) s3) (fun x : A => f x)) *)
  intros A B l ls f s1 s2 s3 H1 H2 H3.
(* Goal: @set_incl (option B) (@setU (option B) (@imset B (option B) (@Some B) s1) (@imset B (option B) (@Some B) s2)) (@bigcup A (option B) (@setI A (@seq_In A (@cons A l ls)) s3) (fun x : A => f x)) *)
  rewrite imset_union_set_eq. apply setU_l_subset.
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  - intros x Hs1. eexists l; split; eauto.
(* Goal: is_true (@isSome A (@Some A x)) *)
    split; eauto. left; eauto.
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  - intros x Hs1. eapply H3 in Hs1.
(* Goal: @bigcup A (option B) (@setI A (@seq_In A (@cons A l ls)) s3) (fun x : A => f x) x *)
    edestruct Hs1 as [x' [[Hs3 Hls] Hin]].
(* Goal: is_true (@isSome A (@Some A x)) *)
    eexists x'; split; eauto. split; eauto.
(* Goal: is_true (@isSome A (@Some A x)) *)
    right; eauto.
Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma imset_set0_subset {A B} (f : A -> B) (s : set B) :
  (f @: set0) \subset s.
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  firstorder.
Qed.

Lemma setI_set_eq_r {A : Type} (s1 s2 s2' : set A) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  s2 <--> s2' ->
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  (s1 :&: s2) <--> (s1 :&: s2').
Proof.
(* Goal: forall _ : @set_eq A s2 s2', @set_eq A (@setI A s1 s2) (@setI A s1 s2') *)
  intros. rewrite H; reflexivity.
Qed.

Lemma isSome_subset {A : Type} (s1 s2 s1' s2' : set (option A)) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  isSome :&: s1 \subset isSome :&: s2 ->
  isSome :&: (s1 :|: ([set None] :&: s1')) \subset isSome :&: (s2 :|: ([set None] :&: s2')).
Proof.
(* Goal: forall _ : @set_incl (option A) (@setI (option A) (fun u : option A => is_true (@isSome A u)) s1) (@setI (option A) (fun u : option A => is_true (@isSome A u)) s2), @set_incl (option A) (@setI (option A) (fun u : option A => is_true (@isSome A u)) (@setU (option A) s1 (@setI (option A) (@set1 (option A) (@None A)) s1'))) (@setI (option A) (fun u : option A => is_true (@isSome A u)) (@setU (option A) s2 (@setI (option A) (@set1 (option A) (@None A)) s2'))) *)
  intros Hyp x [H1 H2]. destruct x as [ x | ]; try discriminate.
(* Goal: is_true (@isSome A (@Some A x)) *)
  split; eauto.
(* Goal: is_true (@isSome A (@Some A x)) *)
  inv H2. left; eauto.
(* Goal: is_true (@isSome A (@Some A x)) *)
  eapply Hyp. now split; eauto.
(* Goal: @setU (option A) s2 (@setI (option A) (@set1 (option A) (@None A)) s2') (@Some A x) *)
  inv H. now inv H0.
Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma bigcup_nil_setI {A B} (f : A -> set B)
      (l : seq A) s :
  \bigcup_(x in [] :&: s) (f x) \subset
  \bigcup_(x in (l :&: s)) (f x).
Proof.
(* Goal: @bigcup A B (@setI A (@seq_In A l) s) (fun x : A => f x) z *)
  intros z [y [[Hin1 _] Hin2]]. inv Hin1.
Qed.

Lemma isSome_set_eq {A} (s : set (option A)) (s' : set A) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  s \subset (Some @: s') :|: [set None] ->
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  Some @: s' \subset s ->
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  isSome :&: s <--> Some @: s'.
Proof.
(* Goal: @setI (option A) (fun u : option A => is_true (@isSome A u)) s (@Some A y) *)
  intros H1 H2 x; split.
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  - intros [H3 H4]. destruct x; try discriminate.
(* Goal: @imset A (option A) (@Some A) s' (@Some A a) *)
(* Goal: forall _ : @imset A (option A) (@Some A) s' x, @setI (option A) (fun u : option A => is_true (@isSome A u)) s x *)
    eapply H1 in H4. inv H4; try discriminate.
(* Goal: f y a *)
    eassumption. 
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  - intros [y [H3 H4]].
(* Goal: @setI (option A) (fun u : option A => is_true (@isSome A u)) s (@Some A y) *)
    inv H4. split. now eauto.
(* Goal: s (@Some A y) *)
    eapply H2.
(* Goal: @imset A (option A) (@Some A) s' (@Some A y) *)
    eexists; split; eauto.
Qed.

Lemma set_eq_isSome_sound {A} (s : set (option A)) (s' : set A) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  isSome :&: s <--> Some @: s' ->
  s \subset (Some @: s') :|: [set None].
Proof.
(* Goal: forall _ : @set_eq (option A) (@setI (option A) (fun u : option A => is_true (@isSome A u)) s) (@imset A (option A) (@Some A) s'), @set_incl (option A) s (@setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A))) *)
  intros H [x| ] Hin.
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  - left. eapply H.
(* Goal: @setI (option A) (fun u : option A => is_true (@isSome A u)) s (@Some A x) *)
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
    eexists; eauto.
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  - right; reflexivity.
Qed.

Lemma set_eq_isSome_complete {A} (s : set (option A)) (s' : set A) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  isSome :&: s <--> Some @: s' ->
  Some @: s' \subset s.
Proof.
(* Goal: @set_eq U (@bigcup T U s1 (fun x : T => @setI U s2 (F x))) (@setI U s2 (@bigcup T U s1 (fun x : T => F x))) *)
  intros H. rewrite <- H. firstorder.
Qed.

Definition somes {A} (s : set (option A)) : set A :=
  [set x | Some x \in s].

Lemma somes_subset {A} (s1 s2 : set (option A)) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  s1 \subset s2 ->
  somes s1 \subset somes s2.
Proof.
(* Goal: forall _ : @set_incl (option A) s1 s2, @set_incl A (@somes A s1) (@somes A s2) *)
  intros Hs a.
(* Goal: forall _ : @somes A s1 a, @somes A s2 a *)
  apply Hs.
Qed.

(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
Lemma bigcup_somes {A B} (sA : set A) (s : A -> set (option B)) :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  somes (\bigcup_(a in sA) s a) <--> \bigcup_(a in sA) somes (s a).
Proof.
(* Goal: @set_eq B (@somes B (@bigcup A (option B) sA (fun a : A => s a))) (@bigcup A B sA (fun a : A => @somes B (s a))) *)
  intro b; split; intros [a Ha]; eexists a; auto.
Qed.

Instance proper_somes A : Morphisms.Proper (set_eq ==> set_eq) (@somes A).
Proof. firstorder. Qed.

Lemma bigcup_setI {T U} (s1 : set T) (s2 : set U) F :
(* Goal: @setU (option A) (@imset A (option A) (@Some A) s') (@set1 (option A) (@None A)) (@None A) *)
  \bigcup_(x in s1) (s2 :&: F x) <--> s2 :&: \bigcup_(x in s1) (F x).
Proof. firstorder. Qed.
