diff --git a/set.v b/set.v
new file mode 100644
index 0000000..bf71a6d
--- /dev/null
+++ b/set.v
@@ -0,0 +1,1091 @@
+From HB Require Import structures.
+Set Warnings "-notation-incompatible-format".
+From mathcomp Require Import ssreflect ssrbool eqtype ssrfun ssrnat choice seq.
+Set Warnings "notation-incompatible-format".
+From mathcomp Require Import fintype tuple bigop path.
+
+(***********************************************************************)
+(*               Experimental library of generic sets                  *)
+(*               ====================================                  *)
+(* Contains two structures:                                            *)
+(*  semisetType == families of sets, without total set (e.g. {fset T}) *)
+(*      setType == families of sets, with total set                    *)
+(*                 (e.g. {set T} or {SAset R^n})                       *)
+(***********************************************************************)
+
+From mathcomp Require Import order.
+
+Declare Scope abstract_set_scope.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Reserved Notation "x \subset y" (at level 70, y at next level).
+Reserved Notation "x \superset y" (at level 70, y at next level).
+Reserved Notation "x \proper y" (at level 70, y at next level).
+Reserved Notation "x \superproper y" (at level 70, y at next level).
+Reserved Notation "x \subset y :> T" (at level 70, y at next level).
+Reserved Notation "x \superset y :> T" (at level 70, y at next level).
+Reserved Notation "x \proper y :> T" (at level 70, y at next level).
+Reserved Notation "x \superproper y :> T" (at level 70, y at next level).
+Reserved Notation "\subsets y" (at level 35).
+Reserved Notation "\supersets y" (at level 35).
+Reserved Notation "\propersets y" (at level 35).
+Reserved Notation "\superpropersets y" (at level 35).
+Reserved Notation "\subsets y :> T" (at level 35, y at next level).
+Reserved Notation "\supersets y :> T" (at level 35, y at next level).
+Reserved Notation "\propersets y :> T" (at level 35, y at next level).
+Reserved Notation "\superpropersets y :> T" (at level 35, y at next level).
+
+Reserved Notation "x \subset y \subset z" (at level 70, y, z at next level).
+Reserved Notation "x \proper y \subset z" (at level 70, y, z at next level).
+Reserved Notation "x \subset y \proper z" (at level 70, y, z at next level).
+Reserved Notation "x \proper y \proper z" (at level 70, y, z at next level).
+Reserved Notation "x \subset y ?= 'iff' c" (at level 70, y, c at next level,
+  format "x '[hv'  \subset  y '/'  ?=  'iff'  c ']'").
+Reserved Notation "x \subset y ?= 'iff' c :> T" (at level 70, y, c at next level,
+  format "x '[hv'  \subset  y '/'  ?=  'iff'  c  :> T ']'").
+
+Reserved Notation "~: A" (at level 35, right associativity).
+Reserved Notation "[ 'set' ~ a ]" (at level 0, format "[ 'set' ~  a ]").
+Reserved Notation "[ 'set' a1 ; a2 ; .. ; an ]"
+ (at level 0, a1 at level 99, format "[ 'set'  a1 ;  a2 ;  .. ;  an ]").
+
+Delimit Scope abstract_set_scope with set.
+Local Open Scope abstract_set_scope.
+
+(* Copy of the ssrbool shim to ensure compatibility with MathComp v1.8.0. *)
+Definition PredType : forall T pT, (pT -> pred T) -> predType T.
+exact PredType || exact mkPredType.
+Defined.
+Arguments PredType [T pT] toP.
+
+Module SET.
+Import Order.Theory.
+
+Fact display_set : unit -> unit. Proof. exact. Qed.
+
+Module Import SetSyntax.
+
+Notation "\sub%set" := (@Order.le (display_set _) _) : abstract_set_scope.
+Notation "\super%set" := (@Order.ge (display_set _) _) : abstract_set_scope.
+Notation "\proper%set" := (@Order.lt (display_set _) _) : abstract_set_scope.
+Notation "\superproper%set" := (@Order.gt (display_set _) _) : abstract_set_scope.
+Notation "\sub?%set" := (@Order.leif (display_set _) _) : abstract_set_scope.
+
+Notation "\subsets y" := (\super%set y) : abstract_set_scope.
+Notation "\subsets y :> T" := (\subsets (y : T)) : abstract_set_scope.
+Notation "\supersets y"  := (\sub%set y) : abstract_set_scope.
+Notation "\supersets y :> T" := (\supersets (y : T)) : abstract_set_scope.
+
+Notation "\propersets y" := (\superproper%set y) : abstract_set_scope.
+Notation "\propersets y :> T" := (\propersets (y : T)) : abstract_set_scope.
+Notation "\superpropersets y" := (\proper%set y) : abstract_set_scope.
+Notation "\superpropersets y :> T" := (\superpropersets (y : T)) : abstract_set_scope.
+
+Notation "x \subset y" := (\sub%set x y) : abstract_set_scope.
+Notation "x \subset y :> T" := ((x : T) \subset (y : T)) : abstract_set_scope.
+Notation "x \superset y" := (\sub%set y x) (only parsing) : abstract_set_scope.
+Notation "x \superset y :> T" := ((y : T) \subset (x : T)) (only parsing) : abstract_set_scope.
+
+Notation "x \proper y"  := (\proper%set x y) : abstract_set_scope.
+Notation "x \proper y :> T" := ((x : T) \proper (y : T)) : abstract_set_scope.
+Notation "x \superproper y"  := (\proper%set y x) (only parsing) : abstract_set_scope.
+Notation "x \superproper y :> T" := ((y : T) \proper (x : T)) (only parsing) : abstract_set_scope.
+
+Notation "x \subset y \subset z" := ((x \subset y)%set && (y \subset z)%set) : abstract_set_scope.
+Notation "x \proper y \subset z" := ((x \proper y)%set && (y \subset z)%set) : abstract_set_scope.
+Notation "x \subset y \proper z" := ((x \subset y)%set && (y \proper z)%set) : abstract_set_scope.
+Notation "x \proper y \proper z" := ((x \proper y)%set && (y \proper z)%set) : abstract_set_scope.
+
+Notation "x \subset y ?= 'iff' C" := (\sub?%set x y C) : abstract_set_scope.
+Notation "x \subset y ?= 'iff' C :> R" := ((x : R) \subset (y : R) ?= iff C)
+  (only parsing) : abstract_set_scope.
+
+Notation set0 := (@Order.bottom (display_set _) _).
+Notation setT := (@Order.top (display_set _) _).
+Notation setU := (@Order.join (display_set _) _).
+Notation setI := (@Order.meet (display_set _) _).
+Notation setD := (@Order.diff (display_set _) _).
+Notation setC := (@Order.compl (display_set _) _).
+
+Notation "x :&: y" := (setI x y).
+Notation "x :|: y" := (setU x y).
+Notation "x :\: y" := (setD x y).
+Notation "~: x"    := (setC x).
+
+Notation "x \subset y" := (\sub%set x y) : bool_scope.
+Notation "x \proper y" := (\proper%set x y) : bool_scope.
+End SetSyntax.
+
+(*Coercion eqType_of_elementType : elementType >-> eqType.*)
+(*Implicit Types (X Y : elementType).*)
+HB.mixin Record isSemiset (elementType : Type (* Universe type *))
+    (eqType_of_elementType : elementType -> eqType)
+    d (set : elementType -> cbDistrLatticeType (display_set d)) := {
+  memset : forall X, set X -> eqType_of_elementType X -> bool;
+  set1 : forall X, eqType_of_elementType X -> set X;
+  notin_set0 : forall X (x : eqType_of_elementType X), ~~ memset _ set0 x; (* set0 is empty instead *)
+  in_set1 : forall X (x y : eqType_of_elementType X), memset _ (set1 _ y) x = (x == y);
+  sub1set : forall X (x : eqType_of_elementType X) A, (set1 _ x \subset A) = (memset _ A x);
+  set_gt0_ex : forall X (A : set X), (set0 \proper A) -> {x | memset _ A x} ; (* exists or sig ?? *)
+  subsetP_subproof : forall X (A B : set X), {subset memset _ A <= memset _ B} -> A \subset B;
+  in_setU : forall X (x : eqType_of_elementType X) A B, (memset _ (A :|: B) x) =
+                    (memset _ A x) || (memset _ B x);
+  (* there is no closure in a set *)
+  funsort : elementType -> elementType -> Type;
+  fun_of_funsort : forall X Y : elementType, funsort X Y -> eqType_of_elementType X -> eqType_of_elementType Y;
+  imset : forall X Y, funsort X Y -> set X -> set Y;
+  FIXME(*couldn't find the name*) : forall X Y (f : funsort X Y) (A : set X) (y : eqType_of_elementType Y),
+    reflect (exists2 x : eqType_of_elementType X, memset _ A x & y = fun_of_funsort _ _ f x)
+            (memset _ (imset _ _ f A) y)
+}.
+
+HB.structure Definition Semiset
+    (elementType : Type)
+    (eqType_of_elementType : elementType -> eqType)
+    d :=
+  {T of @isSemiset elementType eqType_of_elementType d T }.
+
+(* FIXME: how to integrate the constraint Order.CBDistrLattice d T ?
+forall x, Order.hasSub d (T x) ? *)
+
+(* STOP
+
+Record class_of (set : elementType -> Type) := Class {
+  base  : forall X, @Order.CBDistrLattice.class_of (set X);
+  mixin_disp : unit;
+  mixin : mixin_of (fun X => Order.CBDistrLattice.Pack (display_set mixin_disp) (base X))
+}.
+
+
+
+Module Semiset.
+Section ClassDef.
+Variable elementType : Type. (* Universe type *)
+Variable eqType_of_elementType : elementType -> eqType.
+Coercion eqType_of_elementType : elementType >-> eqType.
+Implicit Types (X Y : elementType).
+
+Structure mixin_of d (set : elementType -> (cbDistrLatticeType (display_set d))) :=
+  Mixin {
+  memset : forall X, set X -> X -> bool;
+  set1 : forall X, X -> set X;
+  _ : forall X (x : X), ~~ memset set0 x; (* set0 is empty instead *)
+  _ : forall X (x y : X), memset (set1 y) x = (x == y);
+  _ : forall X (x : X) A, (set1 x \subset A) = (memset A x);
+  _ : forall X (A : set X), (set0 \proper A) -> {x | memset A x} ; (* exists or sig ?? *)
+  _ : forall X (A B : set X), {subset memset A <= memset B} -> A \subset B;
+  _ : forall X (x : X) A B, (memset (A :|: B) x) =
+                    (memset A x) || (memset B x);
+  (* there is no closure in a set *)
+
+  funsort : elementType -> elementType -> Type;
+  fun_of_funsort : forall X Y, funsort X Y -> X -> Y;
+  imset : forall X Y, funsort X Y -> set X -> set Y;
+  _ : forall X Y (f : funsort X Y) (A : set X) (y : Y),
+    reflect (exists2 x : X, memset A x & y = fun_of_funsort f x)
+            (memset (imset f A) y)
+}.
+
+Record class_of (set : elementType -> Type) := Class {
+  base  : forall X, @Order.CBDistrLattice.class_of (set X);
+  mixin_disp : unit;
+  mixin : mixin_of (fun X => Order.CBDistrLattice.Pack (display_set mixin_disp) (base X))
+}.
+
+Local Coercion base : class_of >-> Funclass.
+
+Structure type (disp : unit) := Pack { sort ; _ : class_of sort }.
+
+Local Coercion sort : type >-> Funclass.
+
+Variables (set : elementType -> Type) (disp : unit) (cT : type disp).
+
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Definition clone c & phant_id class c := @Pack disp set c.
+Definition clone_with disp' c of phant_id class c := @Pack disp' set c.
+
+Let xset := let: Pack set _ := cT in set.
+Notation xclass := (class : class_of _ xset).
+
+Definition pack b0
+  (m0 : mixin_of
+ (fun X=> @Order.CBDistrLattice.Pack (display_set disp) (set X) (b0 X))) :=
+  fun bT b &
+ (forall X, phant_id (@Order.CBDistrLattice.class (display_set disp) (bT X)) (b X)) =>
+  fun  disp' m & phant_id m0 m => Pack disp (@Class set b disp' m).
+End ClassDef.
+
+Section CanonicalDef.
+Variable elementType : Type.
+Variable eqType_of_elementType : elementType -> eqType.
+Coercion eqType_of_elementType : elementType >-> eqType.
+Notation type := (type eqType_of_elementType).
+Local Coercion base : class_of >-> Funclass.
+Local Coercion sort : type >-> Funclass.
+Variables (set : elementType -> Type) (X : elementType).
+Variables (disp : unit) (cT : type disp).
+Local Notation ddisp := (display_set disp).
+
+Let xset := let: Pack set _ := cT in set.
+Notation xclass := (@class _ eqType_of_elementType _ cT : class_of eqType_of_elementType xset).
+
+Definition eqType := @Equality.Pack (cT X) (xclass X).
+Definition choiceType := @Choice.Pack (cT X) (xclass X).
+Definition porderType := @Order.POrder.Pack ddisp (cT X) (xclass X).
+Definition latticeType := @Order.Lattice.Pack ddisp (cT X) (xclass X).
+Definition bLatticeType := @Order.BLattice.Pack ddisp (cT X) (xclass X).
+Definition distrLatticeType := @Order.DistrLattice.Pack ddisp (cT X) (xclass X).
+Definition bDistrLatticeType := @Order.BDistrLattice.Pack ddisp (cT X) (xclass X).
+Definition cbDistrLatticeType := @Order.CBDistrLattice.Pack ddisp (cT X) (xclass X).
+End CanonicalDef.
+
+Module Import Exports.
+Coercion mixin      : class_of >-> mixin_of.
+Coercion base       : class_of >-> Funclass.
+Coercion sort       : type >-> Funclass.
+Coercion eqType     : type >-> Equality.type.
+Coercion choiceType : type >-> Choice.type.
+Coercion porderType : type >-> Order.POrder.type.
+Coercion latticeType : type >-> Order.Lattice.type.
+Coercion bLatticeType : type >-> Order.BLattice.type.
+Coercion distrLatticeType : type >-> Order.DistrLattice.type.
+Coercion bDistrLatticeType : type >-> Order.BDistrLattice.type.
+Coercion cbDistrLatticeType : type >-> Order.CBDistrLattice.type.
+
+Canonical eqType.
+Canonical choiceType.
+Canonical porderType.
+Canonical latticeType.
+Canonical bLatticeType.
+Canonical distrLatticeType.
+Canonical bDistrLatticeType.
+Canonical cbDistrLatticeType.
+
+Notation semisetType  := type.
+Notation semisetMixin := mixin_of.
+Notation SemisetMixin := Mixin.
+Notation SemisetType set m := (@pack _ _ set _ _ m _ _ (fun=> id) _ id).
+
+Notation "[ 'semisetType' 'of' set 'for' cset ]" := (@clone _ _ set _ cset _ id)
+  (at level 0, format "[ 'semisetType'  'of'  set  'for'  cset ]") : form_scope.
+Notation "[ 'semisetType' 'of' set 'for' cset 'with' disp ]" :=
+  (@clone_with _ _ set _ cset _ disp _ id)
+  (at level 0, format "[ 'semisetType'  'of'  set  'for'  cset  'with'  disp ]") : form_scope.
+Notation "[ 'semisetType' 'of' set ]" := [semisetType of set for _]
+  (at level 0, format "[ 'semisetType'  'of'  set ]") : form_scope.
+Notation "[ 'semisetType' 'of' set 'with' disp ]" := [semisetType of set for _ with disp]
+  (at level 0, format "[ 'semisetType'  'of'  set  'with' disp ]") : form_scope.
+
+End Exports.
+End Semiset.
+
+Import Semiset.Exports.
+
+Section SemisetOperations.
+Context {elementType : Type} {eqType_of_elementType : elementType -> eqType}.
+Coercion eqType_of_elementType : elementType >-> eqType.
+Context {disp : unit}.
+
+Section setfun.
+Variable (set : semisetType eqType_of_elementType disp).
+Definition setfun := Semiset.funsort (Semiset.class set).
+Definition fun_of_setfun X Y (f : setfun X Y) : X -> Y :=
+  @Semiset.fun_of_funsort _ _ _ _ (Semiset.class set) _ _ f.
+Coercion fun_of_setfun : setfun >-> Funclass.
+End setfun.
+Context {set : semisetType eqType_of_elementType disp}.
+Variable X Y : elementType.
+
+Definition memset : set X -> X -> bool :=
+  @Semiset.memset _ _ _ _ (Semiset.class set) _.
+Definition set1 : X -> set X :=
+  @Semiset.set1 _ _ _ _ (Semiset.class set) _.
+Definition imset : setfun set X Y -> set X -> set Y:=
+  @Semiset.imset _ _ _ _ (Semiset.class set) _ _.
+
+Canonical set_predType := PredType memset.
+
+Structure setpredType := SetPredType {
+  setpred_sort :> Type;
+  tosetpred : setpred_sort -> pred X;
+  _ : {pred_fset : setpred_sort -> set X |
+       forall p x, x \in pred_fset p = tosetpred p x}
+}.
+
+Canonical setpredType_predType (fpX : setpredType) :=
+  @PredType X (setpred_sort fpX) (@tosetpred fpX).
+
+Definition predset (fpX : setpredType) : fpX -> set X :=
+  let: SetPredType _ _ (exist pred_fset _) := fpX in pred_fset.
+
+End SemisetOperations.
+
+Module Import SemisetSyntax.
+
+Notation "[ 'set' x : T | P ]" := (predset (fun x : T => P%B))
+  (at level 0, x at level 99, only parsing) : abstract_set_scope.
+Notation "[ 'set' x | P ]" := [set x : _ | P]
+  (at level 0, x, P at level 99, format "[ 'set'  x  |  P ]") : abstract_set_scope.
+Notation "[ 'set' x 'in' A ]" := [set x | x \in A]
+  (at level 0, x at level 99, format "[ 'set'  x  'in'  A ]") : abstract_set_scope.
+Notation "[ 'set' x : T 'in' A ]" := [set x : T | x \in A]
+  (at level 0, x at level 99, only parsing) : abstract_set_scope.
+Notation "[ 'set' x : T | P & Q ]" := [set x : T | P && Q]
+  (at level 0, x at level 99, only parsing) : abstract_set_scope.
+Notation "[ 'set' x | P & Q ]" := [set x | P && Q ]
+  (at level 0, x, P at level 99, format "[ 'set'  x  |  P  &  Q ]") : abstract_set_scope.
+Notation "[ 'set' x : T 'in' A | P ]" := [set x : T | x \in A & P]
+  (at level 0, x at level 99, only parsing) : abstract_set_scope.
+Notation "[ 'set' x 'in' A | P ]" := [set x | x \in A & P]
+  (at level 0, x at level 99, format "[ 'set'  x  'in'  A  |  P ]") : abstract_set_scope.
+Notation "[ 'set' x 'in' A | P & Q ]" := [set x in A | P && Q]
+  (at level 0, x at level 99,
+   format "[ 'set'  x  'in'  A  |  P  &  Q ]") : abstract_set_scope.
+Notation "[ 'set' x : T 'in' A | P & Q ]" := [set x : T in A | P && Q]
+  (at level 0, x at level 99, only parsing) : abstract_set_scope.
+
+Notation "[ 'set' a ]" := (set1 a)
+  (at level 0, a at level 99, format "[ 'set'  a ]") : abstract_set_scope.
+Notation "[ 'set' a : T ]" := [set (a : T)]
+  (at level 0, a at level 99, format "[ 'set'  a   :  T ]") : abstract_set_scope.
+
+Notation "a |: y" := ([set a] :|: y) : abstract_set_scope.
+Notation "x :\ a" := (x :\: [set a]) : abstract_set_scope.
+Notation "[ 'set' a1 ; a2 ; .. ; an ]" := (setU .. (a1 |: [set a2]) .. [set an]).
+
+Notation "f @: A" := (imset f A) (at level 24) : abstract_set_scope.
+
+End SemisetSyntax.
+
+
+Module Import SemisetTheory.
+Section SemisetTheory.
+
+Variable elementType : Type.
+Variable eqType_of_elementType : elementType -> eqType.
+Coercion eqType_of_elementType : elementType >-> eqType.
+Variable disp : unit.
+Variable set : semisetType eqType_of_elementType disp.
+
+Section setX.
+
+Variables X : elementType.
+Implicit Types (x y : X) (A B C : set X).
+
+Lemma notin_set0 (x : X) : x \notin (set0 : set X).
+Proof.
+rewrite /set1 /in_mem /= /memset.
+case: set => [S [base ? [memset set1 /= H ? ? ? ? ? ? ? ? ?]]] /=.
+exact: H.
+Qed.
+
+Lemma in_set1 x y : x \in ([set y] : set X) = (x == y).
+Proof.
+rewrite /set1 /in_mem /= /memset.
+case: set => [S [base ? [memset set1 /= ? H ? ? ? ? ? ? ? ?]]] /=.
+exact: H.
+Qed.
+
+Lemma sub1set x A : ([set x] \subset A) = (x \in A).
+Proof.
+rewrite /set1 /in_mem /= /memset.
+case: set A => [S [base ? [memset set1 /= ? ? H ? ? ? ? ? ? ?]]] A /=.
+exact: H.
+Qed.
+
+Lemma set_gt0_ex A : set0 \proper A -> {x | x \in A}.
+Proof.
+rewrite /set1 /in_mem /= /memset.
+case: set A => [S [base ? [memset set1 /= ? ? ? H ? ? ? ? ? ?]]] A /=.
+exact: H.
+Qed.
+
+Lemma subsetP_subproof A B : {subset A <= B} -> A \subset B.
+Proof.
+rewrite /set1 /in_mem /= /memset.
+case: set A B => [S [base ? [memset set1 /= ? ? ? ? H ? ? ? ? ?]]] /=.
+exact: H.
+Qed.
+
+Lemma in_setU (x : X) A B : (x \in A :|: B) = (x \in A) || (x \in B).
+Proof.
+rewrite /set1 /in_mem /= /memset.
+case: set A B => [S [base ? [memset set1 /= ? ? ? ? ? H ? ? ? ?]]] /=.
+exact: H.
+Qed.
+
+Lemma in_set0 x : x \in (set0 : set X) = false.
+Proof. by rewrite (negPf (notin_set0 _)). Qed.
+
+Lemma subsetP {A B} : reflect {subset A <= B} (A <= B)%O.
+Proof.
+apply: (iffP idP) => [sAB x xA|/subsetP_subproof//].
+by rewrite -sub1set (le_trans _ sAB) // sub1set.
+Qed.
+
+Lemma setP A B : A =i B <-> A = B.
+Proof.
+split=> [eqAB|->//]; apply/eqP; rewrite eq_le.
+gen have leAB : A B eqAB / A \subset B; last by rewrite !leAB.
+by apply/subsetP => x; rewrite eqAB.
+Qed.
+
+Lemma set1_neq0 (x : X) : [set x] != set0 :> set X.
+Proof. by apply/negP=> /eqP /setP /(_ x); rewrite in_set0 in_set1 eqxx. Qed.
+
+Lemma set1_eq0 x : ([set x] == set0 :> set X) = false.
+Proof. by rewrite (negPf (set1_neq0 _)). Qed.
+
+Lemma set11 x : x \in ([set x] : set X).
+Proof. by rewrite -sub1set. Qed.
+Hint Resolve set11 : core.
+
+Lemma set1_inj : injective (@set1 _ _ _ set X).
+Proof.
+move=> x y /eqP; rewrite eq_le sub1set => /andP [].
+by rewrite in_set1 => /eqP.
+Qed.
+
+Lemma set_0Vmem A : (A = set0) + {x : X | x \in A}.
+Proof.
+have [|AN0] := eqVneq A set0; [left|right] => //.
+by move: AN0; rewrite -lt0x => /set_gt0_ex.
+Qed.
+
+Lemma set0Pn A : reflect (exists x, x \in A) (A != set0).
+Proof.
+have [->|[x xA]] := set_0Vmem A; rewrite ?eqxx -?lt0x.
+  by constructor=> [[x]]; rewrite in_set0.
+suff -> : set0 \proper A by constructor; exists x.
+by move: xA; rewrite -sub1set => /(lt_le_trans _)->; rewrite ?lt0x ?set1_eq0.
+Qed.
+
+Lemma subset1 A x : (A \subset [set x]) = (A == [set x]) || (A == set0).
+Proof.
+symmetry; rewrite eq_le; have [] /= := boolP (A \subset [set x]); last first.
+  by apply: contraNF => /eqP ->; rewrite ?le0x.
+have [/eqP->|[y yA]] := set_0Vmem A; rewrite ?orbT // ?sub1set.
+by move=> /subsetP /(_ _ yA); rewrite in_set1 => /eqP<-; rewrite yA.
+Qed.
+
+Lemma eq_set1 (x : X) A : (A == [set x]) = (set0 \proper A \subset [set x]).
+Proof.
+by rewrite subset1; have [->|?] := posxP A; rewrite 1?eq_sym ?set1_eq0 ?orbF.
+Qed.
+
+Lemma in_setI A B (x : X) : (x \in A :&: B) = (x \in A) && (x \in B).
+Proof.
+apply/idP/idP => [xAB|?]; last by rewrite -sub1set lexI !sub1set.
+by rewrite (subsetP (leIr _ _) _ xAB) (subsetP (leIl _ _) _ xAB).
+Qed.
+
+Lemma set1U A x : [set x] :&: A = if x \in A then [set x] else set0.
+Proof.
+apply/setP => y; rewrite (fun_if (fun E => y \in E)) in_setI in_set1 in_set0.
+by have [->|] := altP (y =P x); rewrite ?if_same //; case: (_ \in A).
+Qed.
+
+Lemma set1U_eq0 A x : ([set x] :&: A == set0) = (x \notin A).
+Proof. by rewrite set1U; case: (x \in A); rewrite ?set1_eq0 ?eqxx. Qed.
+
+Lemma in_setD A B x : (x \in A :\: B) = (x \notin B) && (x \in A).
+Proof.
+apply/idP/idP => [|/andP[xNB xA]]; last first.
+  by rewrite -sub1set leBRL sub1set xA set1U_eq0.
+rewrite -sub1set leBRL sub1set => /andP [-> dxB].
+by rewrite -sub1set disj_le ?set1_eq0.
+Qed.
+
+Definition inE := ((in_set0, in_set1, in_setU, in_setI, in_setD), inE).
+
+Definition subset_trans B A C := (@le_trans _ _ B A C).
+Definition proper_trans B A C := (@lt_trans _ _ B A C).
+Definition sub_proper_trans B A C := (@le_lt_trans _ _ B A C).
+Definition proper_sub_trans B A C := (@lt_le_trans _ _ B A C).
+Definition proper_sub A B := (@ltW _ _ A B).
+
+Lemma properP A B : reflect (A \subset B /\ (exists2 x, x \in B & x \notin A))
+                            (A \proper B).
+Proof.
+apply: (iffP idP)=> [ltAB|[leAB [x xB xNA]]].
+  rewrite ltW //; split => //; have := lt0B ltAB; rewrite lt0x.
+  by move => /set0Pn [x]; rewrite in_setD => /andP [xNA xB]; exists x.
+rewrite lt_neqAle leAB andbT; apply: contraTneq xNA.
+by move=> /setP /(_ x) ->; rewrite xB.
+Qed.
+
+Lemma set1P x y : reflect (x = y) (x \in ([set y] : set X)).
+Proof. by rewrite in_set1; apply/eqP. Qed.
+
+Lemma subset_eqP A B : reflect (A =i B) (A \subset B \subset A)%set.
+Proof.
+apply: (iffP andP) => [[AB BA] x|eqAB]; first by apply/idP/idP; apply: subsetP.
+by split; apply/subsetP=> x; rewrite !eqAB.
+Qed.
+
+Lemma eqEsubset A B : (A == B) = (A \subset B) && (B \subset A).
+Proof. exact: eq_le. Qed.
+
+Lemma properE A B : A \proper B = (A \subset B) && ~~ (B \subset A).
+Proof. by case: comparableP. Qed.
+
+Lemma subEproper A B : A \subset B = (A == B) || (A \proper B).
+Proof. exact: le_eqVlt. Qed.
+
+Lemma eqVproper A B : A \subset B -> A = B \/ A \proper B.
+Proof. by rewrite subEproper => /predU1P. Qed.
+
+Lemma properEneq A B : A \proper B = (A != B) && (A \subset B).
+Proof. exact: lt_neqAle. Qed.
+
+Lemma proper_neq A B : A \proper B -> A != B.
+Proof. by rewrite properEneq; case/andP. Qed.
+
+Lemma eqEproper A B : (A == B) = (A \subset B) && ~~ (A \proper B).
+Proof. by case: comparableP. Qed.
+
+Lemma sub0set A : set0 \subset A.
+Proof. by apply/subsetP=> x; rewrite inE. Qed.
+
+Lemma subset0 A : (A \subset set0) = (A == set0).
+Proof. by rewrite eqEsubset sub0set andbT. Qed.
+
+Lemma proper0 A : (set0 \proper A) = (A != set0).
+Proof. by rewrite properE sub0set subset0. Qed.
+
+Lemma subset_neq0 A B : A \subset B -> A != set0 -> B != set0.
+Proof. by rewrite -!proper0 => sAB /proper_sub_trans->. Qed.
+
+Lemma setU1r x a B : x \in B -> x \in a |: B.
+Proof. by move=> Bx; rewrite !inE predU1r. Qed.
+
+Lemma setU1P x a B : reflect (x = a \/ x \in B) (x \in a |: B).
+Proof. by rewrite !inE; apply: predU1P. Qed.
+
+(* We need separate lemmas for the explicit enumerations since they *)
+(* associate on the left.                                           *)
+Lemma set1Ul x A b : x \in A -> x \in A :|: [set b].
+Proof. by move=> Ax; rewrite !inE Ax. Qed.
+
+Lemma set1Ur A b : b \in A :|: [set b].
+Proof. by rewrite !inE eqxx orbT. Qed.
+
+Lemma setD1P x A b : reflect (x != b /\ x \in A) (x \in A :\ b).
+Proof. by rewrite !inE; apply: andP. Qed.
+
+Lemma in_setD1 x A b : (x \in A :\ b) = (x != b) && (x \in A) .
+Proof. by rewrite !inE. Qed.
+
+Lemma setD11 b A : (b \in A :\ b) = false.
+Proof. by rewrite !inE eqxx. Qed.
+
+Lemma setD1K a A : a \in A -> a |: (A :\ a) = A.
+Proof. by move=> Aa; apply/setP=> x; rewrite !inE; case: eqP => // ->. Qed.
+
+Lemma setU1K a B : a \notin B -> (a |: B) :\ a = B.
+Proof.
+by move/negPf=> nBa; apply/setP=> x; rewrite !inE; case: eqP => // ->.
+Qed.
+
+Lemma set2P x a b : reflect (x = a \/ x = b) (x \in ([set a; b] : set X)).
+Proof. by rewrite !inE; apply: pred2P. Qed.
+
+Lemma in_set2 x a b : (x \in ([set a; b] : set X)) = (x == a) || (x == b).
+Proof. by rewrite !inE. Qed.
+
+Lemma set21 a b : a \in ([set a; b] : set X).
+Proof. by rewrite !inE eqxx. Qed.
+
+Lemma set22 a b : b \in ([set a; b] : set X).
+Proof. by rewrite !inE eqxx orbT. Qed.
+
+Lemma setUP x A B : reflect (x \in A \/ x \in B) (x \in A :|: B).
+Proof. by rewrite !inE; apply: orP. Qed.
+
+Lemma setUC A B : A :|: B = B :|: A.
+Proof. by apply/setP => x; rewrite !inE orbC. Qed.
+
+Lemma setUS A B C : A \subset B -> C :|: A \subset C :|: B.
+Proof.
+move=> sAB; apply/subsetP=> x; rewrite !inE.
+by case: (x \in C) => //; apply: (subsetP sAB).
+Qed.
+
+Lemma setSU A B C : A \subset B -> A :|: C \subset B :|: C.
+Proof. by move=> sAB; rewrite -!(setUC C) setUS. Qed.
+
+Lemma setUSS A B C D : A \subset C -> B \subset D -> A :|: B \subset C :|: D.
+Proof. by move=> /(setSU B) /subset_trans sAC /(setUS C)/sAC. Qed.
+
+Lemma set0U A : set0 :|: A = A.
+Proof. by apply/setP => x; rewrite !inE orFb. Qed.
+
+Lemma setU0 A : A :|: set0 = A.
+Proof. by rewrite setUC set0U. Qed.
+
+Lemma setUA A B C : A :|: (B :|: C) = A :|: B :|: C.
+Proof. by apply/setP => x; rewrite !inE orbA. Qed.
+
+Lemma setUCA A B C : A :|: (B :|: C) = B :|: (A :|: C).
+Proof. by rewrite !setUA (setUC B). Qed.
+
+Lemma setUAC A B C : A :|: B :|: C = A :|: C :|: B.
+Proof. by rewrite -!setUA (setUC B). Qed.
+
+Lemma setUACA A B C D : (A :|: B) :|: (C :|: D) = (A :|: C) :|: (B :|: D).
+Proof. by rewrite -!setUA (setUCA B). Qed.
+
+Lemma setUid A : A :|: A = A.
+Proof. by apply/setP=> x; rewrite inE orbb. Qed.
+
+Lemma setUUl A B C : A :|: B :|: C = (A :|: C) :|: (B :|: C).
+Proof. by rewrite setUA !(setUAC _ C) -(setUA _ C) setUid. Qed.
+
+Lemma setUUr A B C : A :|: (B :|: C) = (A :|: B) :|: (A :|: C).
+Proof. by rewrite !(setUC A) setUUl. Qed.
+
+(* intersection *)
+
+Lemma setIP x A B : reflect (x \in A /\ x \in B) (x \in A :&: B).
+Proof. by rewrite !inE; apply: andP. Qed.
+
+Lemma setIC A B : A :&: B = B :&: A.
+Proof. by apply/setP => x; rewrite !inE andbC. Qed.
+
+Lemma setIS A B C : A \subset B -> C :&: A \subset C :&: B.
+Proof.
+move=> sAB; apply/subsetP=> x; rewrite !inE.
+by case: (x \in C) => //; apply: (subsetP sAB).
+Qed.
+
+Lemma setSI A B C : A \subset B -> A :&: C \subset B :&: C.
+Proof. by move=> sAB; rewrite -!(setIC C) setIS. Qed.
+
+Lemma setISS A B C D : A \subset C -> B \subset D -> A :&: B \subset C :&: D.
+Proof. by move=> /(setSI B) /subset_trans sAC /(setIS C) /sAC. Qed.
+
+Lemma set0I A : set0 :&: A = set0.
+Proof. by apply/setP => x; rewrite !inE andFb. Qed.
+
+Lemma setI0 A : A :&: set0 = set0.
+
+Proof. by rewrite setIC set0I. Qed.
+
+Lemma setIA A B C : A :&: (B :&: C) = A :&: B :&: C.
+Proof. by apply/setP=> x; rewrite !inE andbA. Qed.
+
+Lemma setICA A B C : A :&: (B :&: C) = B :&: (A :&: C).
+Proof. by rewrite !setIA (setIC A). Qed.
+
+Lemma setIAC A B C : A :&: B :&: C = A :&: C :&: B.
+Proof. by rewrite -!setIA (setIC B). Qed.
+
+Lemma setIACA A B C D : (A :&: B) :&: (C :&: D) = (A :&: C) :&: (B :&: D).
+Proof. by rewrite -!setIA (setICA B). Qed.
+
+Lemma setIid A : A :&: A = A.
+Proof. by apply/setP=> x; rewrite inE andbb. Qed.
+
+Lemma setIIl A B C : A :&: B :&: C = (A :&: C) :&: (B :&: C).
+Proof. by rewrite setIA !(setIAC _ C) -(setIA _ C) setIid. Qed.
+
+Lemma setIIr A B C : A :&: (B :&: C) = (A :&: B) :&: (A :&: C).
+Proof. by rewrite !(setIC A) setIIl. Qed.
+
+(* distribute /cancel *)
+
+Lemma setIUr A B C : A :&: (B :|: C) = (A :&: B) :|: (A :&: C).
+Proof. by apply/setP=> x; rewrite !inE andb_orr. Qed.
+
+Lemma setIUl A B C : (A :|: B) :&: C = (A :&: C) :|: (B :&: C).
+Proof. by apply/setP=> x; rewrite !inE andb_orl. Qed.
+
+Lemma setUIr A B C : A :|: (B :&: C) = (A :|: B) :&: (A :|: C).
+Proof. by apply/setP=> x; rewrite !inE orb_andr. Qed.
+
+Lemma setUIl A B C : (A :&: B) :|: C = (A :|: C) :&: (B :|: C).
+Proof. by apply/setP=> x; rewrite !inE orb_andl. Qed.
+
+Lemma setUK A B : (A :|: B) :&: A = A.
+Proof. by apply/setP=> x; rewrite !inE orbK. Qed.
+
+Lemma setKU A B : A :&: (B :|: A) = A.
+Proof. by apply/setP=> x; rewrite !inE orKb. Qed.
+
+Lemma setIK A B : (A :&: B) :|: A = A.
+Proof. by apply/setP=> x; rewrite !inE andbK. Qed.
+
+Lemma setKI A B : A :|: (B :&: A) = A.
+Proof. by apply/setP=> x; rewrite !inE andKb. Qed.
+
+(* difference *)
+
+Lemma setDP A B x : reflect (x \in A /\ x \notin B) (x \in A :\: B).
+Proof. by rewrite inE andbC; apply: andP. Qed.
+
+Lemma setSD A B C : A \subset B -> A :\: C \subset B :\: C.
+Proof.
+by move=> /subsetP AB; apply/subsetP => x; rewrite !inE => /andP[-> /AB].
+Qed.
+
+Lemma setDS A B C : A \subset B -> C :\: B \subset C :\: A.
+Proof.
+move=> /subsetP AB; apply/subsetP => x; rewrite !inE => /andP[].
+by move=> /(contra (AB _)) ->.
+Qed.
+
+Lemma setDSS A B C D : A \subset C -> D \subset B -> A :\: B \subset C :\: D.
+Proof. by move=> /(setSD B) /subset_trans sAC /(setDS C) /sAC. Qed.
+
+Lemma setD0 A : A :\: set0 = A.
+Proof. exact: subx0. Qed.
+
+Lemma set0D A : set0 :\: A = set0.
+Proof. exact: sub0x. Qed.
+
+Lemma setDv A : A :\: A = set0.
+Proof. exact: subxx. Qed.
+
+Lemma setID A B : A :&: B :|: A :\: B = A.
+Proof. exact: joinIB. Qed.
+
+Lemma setDUl A B C : (A :|: B) :\: C = (A :\: C) :|: (B :\: C).
+Proof. exact: subUx. Qed.
+
+Lemma setDUr A B C : A :\: (B :|: C) = (A :\: B) :&: (A :\: C).
+Proof. exact: subxU. Qed.
+
+Lemma setDIl A B C : (A :&: B) :\: C = (A :\: C) :&: (B :\: C).
+Proof. exact: subIx. Qed.
+
+Lemma setIDA A B C : A :&: (B :\: C) = (A :&: B) :\: C.
+Proof. exact: meetxB. Qed.
+
+Lemma setIDAC A B C : (A :\: B) :&: C = (A :&: C) :\: B.
+Proof. exact: meetBx. Qed.
+
+Lemma setDIr A B C : A :\: (B :&: C) = (A :\: B) :|: (A :\: C).
+Proof. exact: subxI. Qed.
+
+Lemma setDDl A B C : (A :\: B) :\: C = A :\: (B :|: C).
+Proof. exact: subBx. Qed.
+
+Lemma setDDr A B C : A :\: (B :\: C) = (A :\: B) :|: (A :&: C).
+Proof. exact: subxB. Qed.
+
+(* other inclusions *)
+
+Lemma subsetIl A B : A :&: B \subset A.
+Proof. by apply/subsetP=> x; rewrite inE; case/andP. Qed.
+
+Lemma subsetIr A B : A :&: B \subset B.
+Proof. by apply/subsetP=> x; rewrite inE; case/andP. Qed.
+
+Lemma subsetUl A B : A \subset A :|: B.
+Proof. by apply/subsetP=> x; rewrite inE => ->. Qed.
+
+Lemma subsetUr A B : B \subset A :|: B.
+Proof. by apply/subsetP=> x; rewrite inE orbC => ->. Qed.
+
+Lemma subsetU1 x A : A \subset x |: A.
+Proof. exact: subsetUr. Qed.
+
+Lemma subsetDl A B : A :\: B \subset A.
+Proof. exact: leBx. Qed.
+
+Lemma subD1set A x : A :\ x \subset A.
+Proof. by rewrite subsetDl. Qed.
+
+Lemma setIidPl A B : reflect (A :&: B = A) (A \subset B).
+Proof.
+apply: (iffP subsetP) => [sAB | <- x /setIP[] //].
+by apply/setP=> x; rewrite inE; apply/andb_idr/sAB.
+Qed.
+Arguments setIidPl {A B}.
+
+Lemma setIidPr A B : reflect (A :&: B = B) (B \subset A).
+Proof. by rewrite setIC; apply: setIidPl. Qed.
+
+Lemma setUidPl A B : reflect (A :|: B = A) (B \subset A).
+Proof. by rewrite -eq_joinl; apply: eqP. Qed.
+
+Lemma setUidPr A B : reflect (A :|: B = B) (A \subset B).
+Proof. by rewrite setUC; apply: setUidPl. Qed.
+
+Lemma subIset A B C : (B \subset A) || (C \subset A) -> (B :&: C \subset A).
+Proof. by case/orP; apply: subset_trans; rewrite (subsetIl, subsetIr). Qed.
+
+Lemma subsetI A B C : (A \subset B :&: C) = (A \subset B) && (A \subset C).
+Proof.
+rewrite !(sameP setIidPl eqP) setIA; have [-> //| ] := altP (A :&: B =P A).
+by apply: contraNF => /eqP <-; rewrite -setIA -setIIl setIAC.
+Qed.
+
+Lemma subsetIP A B C : reflect (A \subset B /\ A \subset C) (A \subset B :&: C).
+Proof. by rewrite subsetI; apply: andP. Qed.
+
+Lemma subsetIidl A B : (A \subset A :&: B) = (A \subset B).
+Proof. by rewrite subsetI lexx. Qed.
+
+Lemma subsetIidr A B : (B \subset A :&: B) = (B \subset A).
+Proof. by rewrite setIC subsetIidl. Qed.
+
+Lemma subUset A B C : (B :|: C \subset A) = (B \subset A) && (C \subset A).
+Proof. exact: leUx. Qed.
+
+Lemma subsetU A B C : (A \subset B) || (A \subset C) -> A \subset B :|: C.
+Proof. exact: lexU2. Qed.
+
+Lemma subUsetP A B C : reflect (A \subset C /\ B \subset C) (A :|: B \subset C).
+Proof. by rewrite subUset; apply: andP. Qed.
+
+Lemma subDset A B C : (A :\: B \subset C) = (A \subset B :|: C).
+Proof. exact: leBLR. Qed.
+
+Lemma setU_eq0 A B : (A :|: B == set0) = (A == set0) && (B == set0).
+Proof. by rewrite -!subset0 subUset. Qed.
+
+Lemma setD_eq0 A B : (A :\: B == set0) = (A \subset B).
+Proof. by rewrite -subset0 subDset setU0. Qed.
+
+Lemma subsetD1 A B x : (A \subset B :\ x) = (A \subset B) && (x \notin A).
+Proof.
+rewrite andbC; have [xA|] //= := boolP (x \in A).
+  by apply: contraTF isT => /subsetP /(_ x xA); rewrite !inE eqxx.
+move=> xNA; apply/subsetP/subsetP => sAB y yA.
+  by have:= sAB y yA; rewrite !inE => /andP[].
+by rewrite !inE sAB // andbT; apply: contraNneq xNA => <-.
+Qed.
+
+Lemma subsetD1P A B x : reflect (A \subset B /\ x \notin A) (A \subset B :\ x).
+Proof. by rewrite subsetD1; apply: andP. Qed.
+
+Lemma properD1 A x : x \in A -> A :\ x \proper A.
+Proof. by move=> Ax; rewrite properE subsetDl /= subsetD1 Ax andbF. Qed.
+
+Lemma properIr A B : ~~ (B \subset A) -> A :&: B \proper B.
+Proof. by move=> nsAB; rewrite properE subsetIr subsetI negb_and nsAB. Qed.
+
+Lemma properIl A B : ~~ (A \subset B) -> A :&: B \proper A.
+Proof. by move=> nsBA; rewrite properE subsetIl subsetI negb_and nsBA orbT. Qed.
+
+Lemma properUr A B : ~~ (A \subset B) ->  B \proper A :|: B.
+Proof. by rewrite properE subsetUr subUset lexx /= andbT. Qed.
+
+Lemma properUl A B : ~~ (B \subset A) ->  A \proper A :|: B.
+Proof. by move=> not_sBA; rewrite setUC properUr. Qed.
+
+Lemma proper1set A x : ([set x] \proper A) -> (x \in A).
+Proof. by move/proper_sub; rewrite sub1set. Qed.
+
+Lemma properIset A B C : (B \proper A) || (C \proper A) -> (B :&: C \proper A).
+Proof. by case/orP; apply: sub_proper_trans; rewrite (subsetIl, subsetIr). Qed.
+
+Lemma properI A B C : (A \proper B :&: C) -> (A \proper B) && (A \proper C).
+Proof.
+move=> pAI; apply/andP.
+by split; apply: (proper_sub_trans pAI); rewrite (subsetIl, subsetIr).
+Qed.
+
+Lemma properU A B C : (B :|: C \proper A) -> (B \proper A) && (C \proper A).
+Proof.
+move=> pUA; apply/andP.
+by split; apply: sub_proper_trans pUA; rewrite (subsetUr, subsetUl).
+Qed.
+
+End setX.
+
+Section setXY.
+
+Variables X Y : elementType.
+Implicit Types (x : X) (y : Y) (A : set X) (B : set Y) (f : setfun set X Y).
+
+Lemma imsetP (f : setfun set X Y) A y :
+    reflect (exists2 x : X, x \in A & y = f x) (y \in imset f A).
+Proof.
+move: A f; rewrite /set1 /in_mem /= /memset /imset /setfun.
+case: set => [S [base ? [memset set1 /= ? ? ? ? ? ? ? ? ? H]]] /= A f.
+exact: H.
+Qed.
+
+Lemma mem_imset f A x : x \in A -> f x \in imset f A.
+Proof. by move=> Dx; apply/imsetP; exists x. Qed.
+
+Lemma imset0 f : imset f set0 = set0.
+Proof.
+apply/setP => y; rewrite in_set0.
+by apply/imsetP => [[x]]; rewrite in_set0.
+Qed.
+
+Lemma imset_eq0 f A : (imset f A == set0) = (A == set0).
+Proof.
+have [->|/set_gt0_ex [x xA]] := posxP A; first by rewrite imset0 eqxx.
+by apply/set0Pn; exists (f x); rewrite mem_imset.
+Qed.
+
+Lemma imset_set1 f x : imset f [set x] = [set f x].
+Proof.
+apply/setP => y.
+by apply/imsetP/set1P=> [[x' /set1P-> //]| ->]; exists x; rewrite ?set11.
+Qed.
+
+Lemma imsetS f A A' : A \subset A' -> imset f A \subset imset f A'.
+Proof.
+move=> leAB; apply/subsetP => y /imsetP [x xA ->].
+by rewrite mem_imset // (subsetP leAB).
+Qed.
+
+Lemma imset_proper f A A' :
+   {in A' &, injective f} -> A \proper A' -> imset f A \proper imset f A'.
+Proof.
+move=> injf /properP[sAB [x Bx nAx]]; rewrite lt_leAnge imsetS //=.
+apply: contra nAx => sfBA.
+have: f x \in imset f A by rewrite (subsetP sfBA) ?mem_imset.
+by case/imsetP=> y Ay /injf-> //; apply: subsetP sAB y Ay.
+Qed.
+
+End setXY.
+
+End SemisetTheory.
+End SemisetTheory.
+
+Module set.
+Section ClassDef.
+Variable elementType : Type.
+Variable eqType_of_elementType : elementType -> eqType.
+Coercion eqType_of_elementType : elementType >-> eqType.
+Implicit Types (X Y : elementType).
+
+Record class_of (set : elementType -> Type) := Class {
+  base  : forall X, Order.CTBDistrLattice.class_of (set X);
+  mixin_disp : unit;
+  mixin : Semiset.mixin_of eqType_of_elementType
+            (fun X => Order.CBDistrLattice.Pack (display_set mixin_disp) (base X))
+}.
+
+Local Coercion base : class_of >-> Funclass.
+Definition base2 (set : elementType -> Type)
+         (c : class_of set) := Semiset.Class (@mixin set c).
+Local Coercion base2 : class_of >-> Semiset.class_of.
+
+Structure type (disp : unit) := Pack { sort ; _ : class_of sort }.
+
+Local Coercion sort : type >-> Funclass.
+
+Variables (set : elementType -> Type) (disp : unit) (cT : type disp).
+
+Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
+Let xset := let: Pack set _ := cT in set.
+Notation xclass := (class : class_of xset).
+
+Definition pack :=
+  fun bT (b : forall X, Order.CTBDistrLattice.class_of _)
+      & (forall X, phant_id (@Order.CTBDistrLattice.class disp (bT X)) (b X)) =>
+  fun d' mT m & phant_id (@Semiset.class _ eqType_of_elementType mT)
+                      (@Semiset.Class _ _ set b d' m) =>
+  Pack disp (@Class set (fun x => b x) _ m).
+
+End ClassDef.
+
+Section CanonicalDef.
+Variable elementType : Type.
+Variable eqType_of_elementType : elementType -> eqType.
+Coercion eqType_of_elementType : elementType >-> eqType.
+Notation type := (type eqType_of_elementType).
+Local Coercion sort : type >-> Funclass.
+Local Coercion base : class_of >-> Funclass.
+Local Coercion base2 : class_of >-> Semiset.class_of.
+Variables (set : elementType -> Type) (X : elementType).
+Variable (disp : unit) (cT : type disp).
+Local Notation ddisp := (display_set disp).
+
+Let xset := let: Pack set _ := cT in set.
+Notation xclass := (@class _ eqType_of_elementType _ cT : class_of eqType_of_elementType xset).
+
+Definition eqType := @Equality.Pack (cT X) (xclass X).
+Definition choiceType := @Choice.Pack (cT X) (xclass X).
+Definition porderType := @Order.POrder.Pack ddisp (cT X) (xclass X).
+Definition latticeType := @Order.Lattice.Pack ddisp (cT X) (xclass X).
+Definition bLatticeType := @Order.BLattice.Pack ddisp (cT X) (xclass X).
+Definition distrLatticeType := @Order.DistrLattice.Pack ddisp (cT X) (xclass X).
+Definition bDistrLatticeType := @Order.BDistrLattice.Pack ddisp (cT X) (xclass X).
+Definition cbDistrLatticeType := @Order.CBDistrLattice.Pack ddisp (cT X) (xclass X).
+Definition ctbDistrLatticeType := @Order.CTBDistrLattice.Pack ddisp (cT X) (xclass X).
+Definition semisetType := @Semiset.Pack _ _ disp cT xclass.
+Definition semiset_ctbDistrLatticeType :=
+  @Order.CTBDistrLattice.Pack ddisp (semisetType X) (xclass X).
+End CanonicalDef.
+
+Module Import Exports.
+Coercion base      : class_of >-> Funclass.
+Coercion base2     : class_of >-> Semiset.class_of.
+Coercion sort      : type >-> Funclass.
+Coercion eqType    : type >-> Equality.type.
+Coercion choiceType : type >-> Choice.type.
+Coercion porderType : type >-> Order.POrder.type.
+Coercion latticeType : type >-> Order.Lattice.type.
+Coercion bLatticeType : type >-> Order.BLattice.type.
+Coercion distrLatticeType : type >-> Order.DistrLattice.type.
+Coercion bDistrLatticeType : type >-> Order.BDistrLattice.type.
+Coercion cbDistrLatticeType : type >-> Order.CBDistrLattice.type.
+Coercion ctbDistrLatticeType : type >-> Order.CTBDistrLattice.type.
+Coercion semisetType : type >-> Semiset.type.
+
+Canonical eqType.
+Canonical choiceType.
+Canonical porderType.
+Canonical latticeType.
+Canonical bLatticeType.
+Canonical distrLatticeType.
+Canonical bDistrLatticeType.
+Canonical cbDistrLatticeType.
+Canonical ctbDistrLatticeType.
+Canonical semisetType.
+
+Notation setType  := type.
+
+Notation "[ 'setType' 'of' set ]" := (@pack _ _ set _ _ _ (fun=> id) _ _ _ id)
+  (at level 0, format "[ 'setType'  'of'  set ]") : form_scope.
+
+End Exports.
+End set.
+
+Import set.Exports.
+
+Module Import setTheory.
+Section setTheory.
+
+Variable elementType : Type.
+Variable eqType_of_elementType : elementType -> eqType.
+Coercion eqType_of_elementType : elementType >-> eqType.
+Variable disp : unit.
+Variable set : setType eqType_of_elementType disp.
+
+Section setX.
+
+Variables X : elementType.
+Implicit Types (x y : X) (A B : set X).
+
+
+End setX.
+
+End setTheory.
+End setTheory.
+
+Module Theory.
+
+Export Semiset.Exports.
+Export set.Exports.
+Export SetSyntax.
+Export SemisetSyntax.
+Export SemisetTheory.
+Export setTheory.
+
+End Theory.
+
+*)
+
+End SET.