diff --git a/FSet.v b/FSet.v
deleted file mode 100644
index fa28cc3..0000000
--- a/FSet.v
+++ /dev/null
@@ -1,638 +0,0 @@
-Require Import HoTT.
-Require Export HoTT.
-Require Import FunextAxiom.
-
-Module Export FinSet.
-
-Section FSet.
-Variable A : Type.
-
-Private Inductive FSet : Type :=
-  | E : FSet
-  | L : A -> FSet
-  | U : FSet -> FSet -> FSet.
-
-Notation "{| x |}" :=  (L x).
-Infix "∪" := U (at level 8, right associativity).
-Notation "∅" := E.
-
-Axiom assoc : forall (x y z : FSet ),
-  x ∪ (y ∪ z) = (x ∪ y) ∪ z.
-
-Axiom comm : forall (x y : FSet),
-  x ∪ y = y ∪ x.
-
-Axiom nl : forall (x : FSet),
-  ∅ ∪ x = x.
-
-Axiom nr : forall (x : FSet),
-  x ∪ ∅ = x.
-
-Axiom idem : forall (x : A),
-  {| x |} ∪ {|x|} = {|x|}.
-
-Axiom trunc : IsHSet FSet.
-
-Fixpoint FSet_rec
-  (P : Type)
-  (H: IsHSet P)
-  (e : P)
-  (l : A -> P)
-  (u : P -> P -> P)
-  (assocP : forall (x y z : P), u x (u y z) = u (u x y) z)
-  (commP : forall (x y : P), u x y = u y x)
-  (nlP : forall (x : P), u e x = x)
-  (nrP : forall (x : P), u x e = x)
-  (idemP : forall (x : A), u (l x) (l x) = l x)
-  (x : FSet)
-  {struct x}
-  : P
-  := (match x return _ -> _ -> _ -> _ -> _ -> _ -> P with
-        | E => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => e
-        | L a => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => l a
-        | U y z => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => u 
-           (FSet_rec P H e l u assocP commP nlP nrP idemP y)
-           (FSet_rec P H e l u assocP commP nlP nrP idemP z)
-      end) assocP commP nlP nrP idemP H.
-
-Axiom FSet_rec_beta_assoc : forall
-  (P : Type)
-  (H: IsHSet P)
-  (e : P)
-  (l : A -> P)
-  (u : P -> P -> P)
-  (assocP : forall (x y z : P), u x (u y z) = u (u x y) z)
-  (commP : forall (x y : P), u x y = u y x)
-  (nlP : forall (x : P), u e x = x)
-  (nrP : forall (x : P), u x e = x)
-  (idemP : forall (x : A), u (l x) (l x) = l x)
-  (x y z : FSet),
-  ap (FSet_rec P H e l u assocP commP nlP nrP idemP) (assoc x y z) 
-  =
-  (assocP (FSet_rec P H e l u assocP commP nlP nrP idemP x)
-          (FSet_rec P H e l u assocP commP nlP nrP idemP y)
-          (FSet_rec P H e l u assocP commP nlP nrP idemP z)
-  ).
-
-Axiom FSet_rec_beta_comm : forall
-  (P : Type)
-  (H: IsHSet P)
-  (e : P)
-  (l : A -> P)
-  (u : P -> P -> P)
-  (assocP : forall (x y z : P), u x (u y z) = u (u x y) z)
-  (commP : forall (x y : P), u x y = u y x)
-  (nlP : forall (x : P), u e x = x)
-  (nrP : forall (x : P), u x e = x)
-  (idemP : forall (x : A), u (l x) (l x) = l x)
-  (x y : FSet),
-  ap (FSet_rec P H e l u assocP commP nlP nrP idemP) (comm x y)
-  =
-  (commP (FSet_rec P H e l u assocP commP nlP nrP idemP x)
-         (FSet_rec P H e l u assocP commP nlP nrP idemP y)
-  ).
-
-Axiom FSet_rec_beta_nl : forall
-  (P : Type)
-  (H: IsHSet P)
-  (e : P)
-  (l : A -> P)
-  (u : P -> P -> P)
-  (assocP : forall (x y z : P), u x (u y z) = u (u x y) z)
-  (commP : forall (x y : P), u x y = u y x)
-  (nlP : forall (x : P), u e x = x)
-  (nrP : forall (x : P), u x e = x)
-  (idemP : forall (x : A), u (l x) (l x) = l x)
-  (x : FSet),
-  ap (FSet_rec P H e l u assocP commP nlP nrP idemP) (nl x)
-  =
-  (nlP (FSet_rec P H e l u assocP commP nlP nrP idemP x)
-  ).
-
-Axiom FSet_rec_beta_nr : forall
-  (P : Type)
-  (H: IsHSet P)
-  (e : P)
-  (l : A -> P)
-  (u : P -> P -> P)
-  (assocP : forall (x y z : P), u x (u y z) = u (u x y) z)
-  (commP : forall (x y : P), u x y = u y x)
-  (nlP : forall (x : P), u e x = x)
-  (nrP : forall (x : P), u x e = x)
-  (idemP : forall (x : A), u (l x) (l x) = l x)
-  (x : FSet),
-  ap (FSet_rec P H e l u assocP commP nlP nrP idemP) (nr x)
-  =
-  (nrP (FSet_rec P H e l u assocP commP nlP nrP idemP x)
-  ).
-
-Axiom FSet_rec_beta_idem : forall
-  (P : Type)
-  (H: IsHSet P)
-  (e : P)
-  (l : A -> P)
-  (u : P -> P -> P)
-  (assocP : forall (x y z : P), u x (u y z) = u (u x y) z)
-  (commP : forall (x y : P), u x y = u y x)
-  (nlP : forall (x : P), u e x = x)
-  (nrP : forall (x : P), u x e = x)
-  (idemP : forall (x : A), u (l x) (l x) = l x)
-  (x : A),
-  ap (FSet_rec P H e l u assocP commP nlP nrP idemP) (idem x)
-  =
-  idemP x.
-
-
-(* Induction principle *)
-Fixpoint FSet_ind
-  (P : FSet -> Type)
-  (H :  forall a : FSet, IsHSet (P a))
-  (eP : P E)
-  (lP : forall a: A, P (L a))
-  (uP : forall (x y: FSet), P x -> P y -> P (U x y))
-  (assocP : forall (x y z : FSet) 
-                   (px: P x) (py: P y) (pz: P z),
-  assoc x y z #
-   (uP      x    (U y z)          px        (uP y z py pz)) 
-  = 
-   (uP   (U x y)    z       (uP x y px py)          pz))
-  (commP : forall (x y: FSet) (px: P x) (py: P y),
-  comm x y #
-  uP x y px py = uP y x py px) 
-  (nlP : forall (x : FSet) (px: P x), 
-  nl x # uP E x eP px = px)
-  (nrP : forall (x : FSet) (px: P x), 
-  nr x # uP x E px eP = px)
-  (idemP : forall (x : A), 
-  idem x # uP (L x) (L x) (lP x) (lP x) = lP x)
-  (x : FSet)
-  {struct x}
-  : P x
-  := (match x return _ -> _ -> _ -> _ -> _ -> _ -> P x with
-        | E => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => eP
-        | L a => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => lP a
-        | U y z => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => uP y z
-           (FSet_ind P H eP lP uP assocP commP nlP nrP idemP y)
-           (FSet_ind P H eP lP uP assocP commP nlP nrP idemP z)
-      end) H assocP commP nlP nrP idemP.
-
-
-Axiom FSet_ind_beta_assoc : forall
-  (P : FSet -> Type)
-  (H :  forall a : FSet, IsHSet (P a))
-  (eP : P E)
-  (lP : forall a: A, P (L a))
-  (uP : forall (x y: FSet), P x -> P y -> P (U x y))
-  (assocP : forall (x y z : FSet) 
-                   (px: P x) (py: P y) (pz: P z),
-  assoc x y z #
-   (uP      x    (U y z)          px        (uP y z py pz)) 
-  = 
-   (uP   (U x y)    z       (uP x y px py)          pz))
-  (commP : forall (x y: FSet) (px: P x) (py: P y),
-  comm x y #
-  uP x y px py = uP y x py px) 
-  (nlP : forall (x : FSet) (px: P x), 
-  nl x # uP E x eP px = px)
-  (nrP : forall (x : FSet) (px: P x), 
-  nr x # uP x E px eP = px)
-  (idemP : forall (x : A), 
-  idem x # uP (L x) (L x) (lP x) (lP x) = lP x)
-  (x y z : FSet),
-  apD (FSet_ind P H eP lP uP assocP commP nlP nrP idemP) 
-      (assoc x y z)
-  =
-  (assocP x y z 
-          (FSet_ind P H eP lP uP assocP commP nlP nrP idemP x)
-          (FSet_ind P H eP lP uP assocP commP nlP nrP idemP y)
-          (FSet_ind P H eP lP uP assocP commP nlP nrP idemP z)
-  ).
-
-
-
-Axiom FSet_ind_beta_comm : forall  
-  (P : FSet -> Type)
-  (H :  forall a : FSet, IsHSet (P a))
-  (eP : P E)
-  (lP : forall a: A, P (L a))
-  (uP : forall (x y: FSet), P x -> P y -> P (U x y))
-  (assocP : forall (x y z : FSet) 
-                   (px: P x) (py: P y) (pz: P z),
-  assoc x y z #
-   (uP      x    (U y z)          px        (uP y z py pz)) 
-  = 
-   (uP   (U x y)    z       (uP x y px py)          pz))
-  (commP : forall (x y : FSet) (px: P x) (py: P y),
-  comm x y #
-  uP x y px py = uP y x py px) 
-  (nlP : forall (x : FSet) (px: P x), 
-  nl x # uP E x eP px = px)
-  (nrP : forall (x : FSet) (px: P x), 
-  nr x # uP x E px eP = px)
-  (idemP : forall (x : A), 
-  idem x # uP (L x) (L x) (lP x) (lP x) = lP x)
-  (x y : FSet),
-  apD (FSet_ind P H eP lP uP assocP commP nlP nrP idemP) (comm x y)
-  =
-  (commP x y 
-         (FSet_ind P H eP lP uP assocP commP nlP nrP idemP x)
-         (FSet_ind P H eP lP uP assocP commP nlP nrP idemP y)
-  ).
-
-Axiom FSet_ind_beta_nl : forall
-  (P : FSet -> Type)
-  (H :  forall a : FSet, IsHSet (P a))
-  (eP : P E)
-  (lP : forall a: A, P (L a))
-  (uP : forall (x y: FSet), P x -> P y -> P (U x y))
-  (assocP : forall (x y z : FSet) 
-                   (px: P x) (py: P y) (pz: P z),
-  assoc x y z #
-   (uP      x    (U y z)          px        (uP y z py pz)) 
-  = 
-   (uP   (U x y)    z       (uP x y px py)          pz))
-  (commP : forall (x y : FSet) (px: P x) (py: P y),
-  comm x y #
-  uP x y px py = uP y x py px) 
-  (nlP : forall (x : FSet) (px: P x), 
-  nl x # uP E x eP px = px)
-  (nrP : forall (x : FSet) (px: P x), 
-  nr x # uP x E px eP = px)
-  (idemP : forall (x : A), 
-  idem x # uP (L x) (L x) (lP x) (lP x) = lP x)
-  (x : FSet),
-  apD (FSet_ind P H eP lP uP assocP commP nlP nrP idemP) (nl x)
-  =
-  (nlP x (FSet_ind P H eP lP uP assocP commP nlP nrP idemP x)
-  ).
-
-Axiom FSet_ind_beta_nr : forall
-  (P : FSet -> Type)
-  (H :  forall a : FSet, IsHSet (P a))
-  (eP : P E)
-  (lP : forall a: A, P (L a))
-  (uP : forall (x y: FSet), P x -> P y -> P (U x y))
-  (assocP : forall (x y z : FSet) 
-                   (px: P x) (py: P y) (pz: P z),
-  assoc x y z #
-   (uP      x    (U y z)          px        (uP y z py pz)) 
-  = 
-   (uP   (U x y)    z       (uP x y px py)          pz))
-  (commP : forall (x y : FSet) (px: P x) (py: P y),
-  comm x y #
-  uP x y px py = uP y x py px) 
-  (nlP : forall (x : FSet) (px: P x), 
-  nl x # uP E x eP px = px)
-  (nrP : forall (x : FSet) (px: P x), 
-  nr x # uP x E px eP = px)
-  (idemP : forall (x : A), 
-  idem x # uP (L x) (L x) (lP x) (lP x) = lP x)
-  (x : FSet),
-  apD (FSet_ind P H eP lP uP assocP commP nlP nrP idemP) (nr x)
-  =
-  (nrP x (FSet_ind P H eP lP uP assocP commP nlP nrP idemP x)
-  ).
-
-Axiom FSet_ind_beta_idem : forall
-  (P : FSet -> Type)
-  (H :  forall a : FSet, IsHSet (P a))
-  (eP : P E)
-  (lP : forall a: A, P (L a))
-  (uP : forall (x y: FSet), P x -> P y -> P (U x y))
-  (assocP : forall (x y z : FSet) 
-                   (px: P x) (py: P y) (pz: P z),
-  assoc x y z #
-   (uP      x    (U y z)          px        (uP y z py pz)) 
-  = 
-   (uP   (U x y)    z       (uP x y px py)          pz))
-  (commP : forall (x y : FSet) (px: P x) (py: P y),
-  comm x y #
-  uP x y px py = uP y x py px) 
-  (nlP : forall (x : FSet) (px: P x), 
-  nl x # uP E x eP px = px)
-  (nrP : forall (x : FSet) (px: P x), 
-  nr x # uP x E px eP = px)
-  (idemP : forall (x : A), 
-  idem x # uP (L x) (L x) (lP x) (lP x) = lP x)
-  (x : A),
-  apD (FSet_ind P H eP lP uP assocP commP nlP nrP idemP) (idem x)
-  =
-  idemP x.
-
-End FSet.
-
-Parameter A : Type.
-Parameter A_eqdec : forall (x y : A), Decidable (x = y).
-Definition deceq (x y : A) :=
-  if dec (x = y) then true else false.
-
-Theorem deceq_sym : forall x y, deceq x y = deceq y x.
-Proof.
-intros x y.
-unfold deceq.
-destruct (dec (x = y)) ; destruct (dec (y = x)) ; cbn.
-- reflexivity. 
-- pose (n (p^)) ; contradiction.
-- pose (n (p^)) ; contradiction.
-- reflexivity.
-Defined.
-
-Arguments E {_}.
-Arguments U {_} _ _.
-Arguments L {_} _.
-
-Theorem idemU : forall x : FSet A, U x x = x.
-Proof.
-simple refine (FSet_ind A _ _ _ _ _ _ _ _ _ _) ; try (intros ; apply set_path2) ; cbn.
-- apply nl.
-- apply idem.
-- intros x y P Q.
-  etransitivity. apply assoc.  
-  etransitivity. apply (ap (fun p => U (U p x) y) (comm A x y)).
-  etransitivity. apply (ap (fun p => U p y) (assoc A y x x))^.
-  etransitivity. apply (ap (fun p => U (U y p) y) P).
-  etransitivity. apply (ap (fun p => U p y) (comm A y x)).
-  etransitivity. apply (assoc A x y y)^.
-  apply (ap (fun p => U x p) Q).
-Defined.
-  
-Definition isIn : A -> FSet A -> Bool.
-Proof.
-intros a.
-simple refine (FSet_rec A _ _ _ _ _ _ _ _ _ _).
-- exact false.
-- intro a'. apply (deceq a a').
-- apply orb. 
-- intros x y z. destruct x; reflexivity.
-- intros x y. destruct x, y; reflexivity.
-- intros x. reflexivity. 
-- intros x. destruct x; reflexivity.
-- intros a'. destruct (deceq a a'); reflexivity.
-Defined.
-
-Definition comprehension : 
-  (A -> Bool) -> FSet A -> FSet A.
-Proof.
-intros P.
-simple refine (FSet_rec A _ _ _ _ _ _ _ _ _ _).
-- apply E.
-- intro a.
-  refine (if (P a) then L a else E).
-- apply U.
-- intros. apply assoc.
-- intros. apply comm.
-- intros. apply nl.
-- intros. apply nr.
-- intros. cbn.  
-  destruct (P x).
-  + apply idem.
-  + apply nl.
-Defined.
-
-Theorem comprehension_or : forall ϕ ψ x,
-    comprehension (fun a => orb (ϕ a) (ψ a)) x = U (comprehension ϕ x) (comprehension ψ x).
-Proof.
-intros ϕ ψ.
-simple refine (FSet_ind A _ _ _ _ _ _ _ _ _ _) ; try (intros ; apply set_path2). 
-- cbn. symmetry ; apply nl.
-- cbn. intros.
-  destruct (ϕ a) ; destruct (ψ a) ; symmetry.
-  * apply idem.
-  * apply nr. 
-  * apply nl.
-  * apply nl.
-- simpl. intros x y P Q.
-  cbn. 
-  rewrite P.
-  rewrite Q.
-  rewrite <- assoc.
-  rewrite (assoc A (comprehension ψ x)).
-  rewrite (comm A (comprehension ψ x) (comprehension ϕ y)).
-  rewrite <- assoc.
-  rewrite <- assoc.
-  reflexivity.
-Defined.
-
-Definition intersection (X Y : FSet A) : FSet A := comprehension (fun (a : A) => isIn a X) Y.
-
-Theorem intersection_idem : forall x, intersection x x = x.
-Proof.
-simple refine (FSet_ind A _ _ _ _ _ _ _ _ _ _) ; try (intros ; apply set_path2) ; cbn.
-- reflexivity.
-- intro a.
-  unfold deceq.
-  destruct (dec (a = a)).
-  * reflexivity.
-  * pose (n idpath) ; contradiction.
-- intros x y P Q.
-  rewrite comprehension_or.
-  rewrite comprehension_or.
-  unfold intersection in P.
-  unfold intersection in Q.
-  rewrite P.
-  rewrite Q.
-Admitted.
-    
-  
-    
-
-Theorem intersection_EX : forall x,
-    intersection E x = E.
-Proof.
-simple refine (FSet_ind A _ _ _ _ _ _ _ _ _ _) ; try (intros ; apply set_path2).
-- reflexivity.
-- intro a.
-  reflexivity.
-- unfold intersection.
-  intros x y P Q.
-  cbn.
-  rewrite P.
-  rewrite Q.
-  apply nl.
-Defined.
-
-Definition intersection_XE x : intersection x E = E := idpath.
-
-Theorem intersection_La : forall a x,
-    intersection (L a) x = if isIn a x then L a else E.
-Proof.
-intro a.
-simple refine (FSet_ind A _ _ _ _ _ _ _ _ _ _) ; try (intros ; apply set_path2).
-- reflexivity.
-- intro b.
-  cbn.
-  rewrite deceq_sym.
-  unfold deceq.
-  destruct (dec (a = b)).
-  * rewrite p ; reflexivity.
-  * reflexivity.
-- unfold intersection.
-  intros x y P Q.
-  cbn.
-  rewrite P.
-  rewrite Q.
-  destruct (isIn a x) ; destruct (isIn a y).
-  * apply idem.
-  * apply nr.
-  * apply nl. 
-  * apply nl.
-Defined.
-
-
-(*
-Theorem intersection_comm : forall x y,
-    intersection x y = intersection y x.
-Proof.
-simple refine (FSet_ind A _ _ _ _ _ _ _ _ _ _) ; cbn.
-- intros.
-  rewrite intersection_E.  
-  reflexivity.
-- intros a.
-  simple refine (FSet_ind A _ _ _ _ _ _ _ _ _ _) ; cbn.
-  * reflexivity.
-  * intro b.
-    admit.
-  * intros x y.
-    destruct (isIn a x) ; destruct (isIn a y) ; intros P Q.
-  + rewrite P.
-    *)
-            
-
-Theorem comp_false : forall x,
-    comprehension (fun _ => false) x = E.
-Proof.
-simple refine (FSet_ind A _ _ _ _ _ _ _ _ _ _) ; try (intros ; apply set_path2) ; cbn.
-- reflexivity.
-- intro a ; reflexivity.
-- intros x y P Q.
-  rewrite P.
-  rewrite Q.
-  apply nl.
-Defined.
-
-(*Theorem union_dist : forall x y z,
-    intersection z (U x y) = U (intersection z x) (intersection z y).
-Proof.
-intros x y.
-simple refine (FSet_ind A _ _ _ _ _ _ _ _ _ _) ; cbn.
-- rewrite intersection_E.
-  rewrite intersection_E.
-  rewrite comp_false.
-  rewrite comp_false.
-  reflexivity.
-- intro a. 
-  *)
-
-Theorem union_dist : forall x y z,
-    intersection (U x y) z = U (intersection x z) (intersection y z).
-Proof.
-simple refine (FSet_ind A _ _ _ _ _ _ _ _ _ _) ; cbn.
-- intros.
-  rewrite nl.
-  rewrite intersection_EX.
-  rewrite nl.
-  reflexivity.
-- intro a.
-  simple refine (FSet_ind A _ _ _ _ _ _ _ _ _ _) ; cbn.
-  * intros.
-    rewrite nr.
-    rewrite intersection_EX.
-    rewrite nr.
-    reflexivity.
-  * intros b.
-    simple refine (FSet_ind A _ _ _ _ _ _ _ _ _ _) ; cbn.
-    + rewrite nl. reflexivity.
-    + intros c.
-      unfold deceq.
-      destruct (dec (c = a)) ; destruct (dec (c = b)) ; cbn.
-      { rewrite idem. reflexivity. }
-      { rewrite nr. reflexivity. }
-      { rewrite nl. reflexivity. }
-      { rewrite nl. reflexivity. }
-    + intros x y P Q.
-      rewrite comprehension_or.
-      rewrite comprehension_or.
-      rewrite assoc.
-      rewrite <- (assoc A (comprehension (fun a0 : A => deceq a0 a) x) (comprehension (fun a0 : A => deceq a0 b) x)).
-      rewrite (comm A (comprehension (fun a0 : A => deceq a0 b) x) (comprehension (fun a0 : A => deceq a0 a) y)).
-      rewrite assoc.
-      rewrite <- assoc.
-      reflexivity.
-    + admit.
-    + admit.
-    + admit.
-    + admit.
-    + admit.
-  * intros x y P Q z.
-    cbn.
-    
-Admitted.
-
-Theorem intersection_isIn : forall a x y,
-    isIn a (intersection x y) = andb (isIn a x) (isIn a y).
-Proof.
-intros a.
-simple refine (FSet_ind A _ _ _ _ _ _ _ _ _ _) ; cbn.
-- intros y.
-  rewrite intersection_EX.
-  reflexivity.
-- intros b y.
-  rewrite intersection_La.
-  unfold deceq.
-  destruct (dec (a = b)) ; cbn.
-  * rewrite p.
-    destruct (isIn b y).
-    + cbn.
-      unfold deceq.
-      destruct (dec (b = b)).
-      { reflexivity. }
-      { pose (n idpath). contradiction. }
-    + reflexivity.
-  * destruct (isIn b y).
-    + cbn.
-      unfold deceq.
-      destruct (dec (a = b)).
-      { pose (n p). contradiction. }
-      { reflexivity. }
-    + reflexivity.
-- intros x y P Q z.
-  rewrite union_dist.
-  cbn.
-  rewrite P.
-  rewrite Q.
-  destruct (isIn a x) ; destruct (isIn a y) ; destruct (isIn a z) ; reflexivity.
-Admitted.
-
-Theorem intersection_assoc x y z :
-    intersection x (intersection y z) = intersection (intersection x y) z.
-Proof.
-simple refine (FSet_ind A _ _ _ _ _ _ _ _ _ _ x) ; cbn ;  try (intros ; apply set_path2).
-- intros.
-  exact _.
-- cbn.
-  rewrite intersection_E.
-  rewrite intersection_E.
-  rewrite intersection_E.
-  reflexivity.
-- intros a y z.
-  cbn.
-  rewrite intersection_La.
-  rewrite intersection_La.
-  rewrite intersection_isIn.
-  destruct (isIn a y).
-  * rewrite intersection_La.
-    destruct (isIn a z).
-    + reflexivity.
-    + reflexivity.
-  * rewrite intersection_E.
-    reflexivity.      
-- unfold intersection. cbn.
-  intros x y P Q z z'.
-  rewrite comprehension_or.
-  rewrite P.
-  rewrite Q.
-  rewrite comprehension_or.
-  cbn.
-  rewrite comprehension_or.
-  reflexivity.
-Admitted.
diff --git a/FinSets.v b/FinSets.v
deleted file mode 100644
index 93a8a4c..0000000
--- a/FinSets.v
+++ /dev/null
@@ -1,532 +0,0 @@
-Require Export HoTT.
-Require Import HitTactics.
-
-Module Export FinSet.
-Section FSet.
-Variable A : Type.
-
-Private Inductive FSet : Type :=
-  | E : FSet
-  | L : A -> FSet
-  | U : FSet -> FSet -> FSet.
-
-Notation "{| x |}" :=  (L x).
-Infix "∪" := U (at level 8, right associativity).
-Notation "∅" := E.
-
-Axiom assoc : forall (x y z : FSet ),
-  x ∪ (y ∪ z) = (x ∪ y) ∪ z.
-
-Axiom comm : forall (x y : FSet),
-  x ∪ y = y ∪ x.
-
-Axiom nl : forall (x : FSet),
-  ∅ ∪ x = x.
-
-Axiom nr : forall (x : FSet),
-  x ∪ ∅ = x.
-
-Axiom idem : forall (x : A),
-  {| x |} ∪ {|x|} = {|x|}.
-
-Axiom trunc : IsHSet FSet.
-
-Fixpoint FSet_rec
-  (P : Type)
-  (H: IsHSet P)
-  (e : P)
-  (l : A -> P)
-  (u : P -> P -> P)
-  (assocP : forall (x y z : P), u x (u y z) = u (u x y) z)
-  (commP : forall (x y : P), u x y = u y x)
-  (nlP : forall (x : P), u e x = x)
-  (nrP : forall (x : P), u x e = x)
-  (idemP : forall (x : A), u (l x) (l x) = l x)
-  (x : FSet)
-  {struct x}
-  : P
-  := (match x return _ -> _ -> _ -> _ -> _ -> _ -> P with
-        | E => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => e
-        | L a => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => l a
-        | U y z => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => u 
-           (FSet_rec P H e l u assocP commP nlP nrP idemP y)
-           (FSet_rec P H e l u assocP commP nlP nrP idemP z)
-      end) assocP commP nlP nrP idemP H.
-
-Axiom FSet_rec_beta_assoc : forall
-  (P : Type)
-  (H: IsHSet P)
-  (e : P)
-  (l : A -> P)
-  (u : P -> P -> P)
-  (assocP : forall (x y z : P), u x (u y z) = u (u x y) z)
-  (commP : forall (x y : P), u x y = u y x)
-  (nlP : forall (x : P), u e x = x)
-  (nrP : forall (x : P), u x e = x)
-  (idemP : forall (x : A), u (l x) (l x) = l x)
-  (x y z : FSet),
-  ap (FSet_rec P H e l u assocP commP nlP nrP idemP) (assoc x y z) 
-  =
-  (assocP (FSet_rec P H e l u assocP commP nlP nrP idemP x)
-          (FSet_rec P H e l u assocP commP nlP nrP idemP y)
-          (FSet_rec P H e l u assocP commP nlP nrP idemP z)
-  ).
-
-Axiom FSet_rec_beta_comm : forall
-  (P : Type)
-  (H: IsHSet P)
-  (e : P)
-  (l : A -> P)
-  (u : P -> P -> P)
-  (assocP : forall (x y z : P), u x (u y z) = u (u x y) z)
-  (commP : forall (x y : P), u x y = u y x)
-  (nlP : forall (x : P), u e x = x)
-  (nrP : forall (x : P), u x e = x)
-  (idemP : forall (x : A), u (l x) (l x) = l x)
-  (x y : FSet),
-  ap (FSet_rec P H e l u assocP commP nlP nrP idemP) (comm x y)
-  =
-  (commP (FSet_rec P H e l u assocP commP nlP nrP idemP x)
-         (FSet_rec P H e l u assocP commP nlP nrP idemP y)
-  ).
-
-Axiom FSet_rec_beta_nl : forall
-  (P : Type)
-  (H: IsHSet P)
-  (e : P)
-  (l : A -> P)
-  (u : P -> P -> P)
-  (assocP : forall (x y z : P), u x (u y z) = u (u x y) z)
-  (commP : forall (x y : P), u x y = u y x)
-  (nlP : forall (x : P), u e x = x)
-  (nrP : forall (x : P), u x e = x)
-  (idemP : forall (x : A), u (l x) (l x) = l x)
-  (x : FSet),
-  ap (FSet_rec P H e l u assocP commP nlP nrP idemP) (nl x)
-  =
-  (nlP (FSet_rec P H e l u assocP commP nlP nrP idemP x)
-  ).
-
-Axiom FSet_rec_beta_nr : forall
-  (P : Type)
-  (H: IsHSet P)
-  (e : P)
-  (l : A -> P)
-  (u : P -> P -> P)
-  (assocP : forall (x y z : P), u x (u y z) = u (u x y) z)
-  (commP : forall (x y : P), u x y = u y x)
-  (nlP : forall (x : P), u e x = x)
-  (nrP : forall (x : P), u x e = x)
-  (idemP : forall (x : A), u (l x) (l x) = l x)
-  (x : FSet),
-  ap (FSet_rec P H e l u assocP commP nlP nrP idemP) (nr x)
-  =
-  (nrP (FSet_rec P H e l u assocP commP nlP nrP idemP x)
-  ).
-
-Axiom FSet_rec_beta_idem : forall
-  (P : Type)
-  (H: IsHSet P)
-  (e : P)
-  (l : A -> P)
-  (u : P -> P -> P)
-  (assocP : forall (x y z : P), u x (u y z) = u (u x y) z)
-  (commP : forall (x y : P), u x y = u y x)
-  (nlP : forall (x : P), u e x = x)
-  (nrP : forall (x : P), u x e = x)
-  (idemP : forall (x : A), u (l x) (l x) = l x)
-  (x : A),
-  ap (FSet_rec P H e l u assocP commP nlP nrP idemP) (idem x)
-  =
-  idemP x.
-
-
-(* Induction principle *)
-Fixpoint FSet_ind
-  (P : FSet -> Type)
-  (H :  forall a : FSet, IsHSet (P a))
-  (eP : P E)
-  (lP : forall a: A, P (L a))
-  (uP : forall (x y: FSet), P x -> P y -> P (U x y))
-  (assocP : forall (x y z : FSet) 
-                   (px: P x) (py: P y) (pz: P z),
-  assoc x y z #
-   (uP      x    (U y z)          px        (uP y z py pz)) 
-  = 
-   (uP   (U x y)    z       (uP x y px py)          pz))
-  (commP : forall (x y: FSet) (px: P x) (py: P y),
-  comm x y #
-  uP x y px py = uP y x py px) 
-  (nlP : forall (x : FSet) (px: P x), 
-  nl x # uP E x eP px = px)
-  (nrP : forall (x : FSet) (px: P x), 
-  nr x # uP x E px eP = px)
-  (idemP : forall (x : A), 
-  idem x # uP (L x) (L x) (lP x) (lP x) = lP x)
-  (x : FSet)
-  {struct x}
-  : P x
-  := (match x return _ -> _ -> _ -> _ -> _ -> _ -> P x with
-        | E => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => eP
-        | L a => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => lP a
-        | U y z => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => uP y z
-           (FSet_ind P H eP lP uP assocP commP nlP nrP idemP y)
-           (FSet_ind P H eP lP uP assocP commP nlP nrP idemP z)
-      end) H assocP commP nlP nrP idemP.
-
-
-Axiom FSet_ind_beta_assoc : forall
-  (P : FSet -> Type)
-  (H :  forall a : FSet, IsHSet (P a))
-  (eP : P E)
-  (lP : forall a: A, P (L a))
-  (uP : forall (x y: FSet), P x -> P y -> P (U x y))
-  (assocP : forall (x y z : FSet) 
-                   (px: P x) (py: P y) (pz: P z),
-  assoc x y z #
-   (uP      x    (U y z)          px        (uP y z py pz)) 
-  = 
-   (uP   (U x y)    z       (uP x y px py)          pz))
-  (commP : forall (x y: FSet) (px: P x) (py: P y),
-  comm x y #
-  uP x y px py = uP y x py px) 
-  (nlP : forall (x : FSet) (px: P x), 
-  nl x # uP E x eP px = px)
-  (nrP : forall (x : FSet) (px: P x), 
-  nr x # uP x E px eP = px)
-  (idemP : forall (x : A), 
-  idem x # uP (L x) (L x) (lP x) (lP x) = lP x)
-  (x y z : FSet),
-  apD (FSet_ind P H eP lP uP assocP commP nlP nrP idemP) 
-      (assoc x y z)
-  =
-  (assocP x y z 
-          (FSet_ind P H eP lP uP assocP commP nlP nrP idemP x)
-          (FSet_ind P H eP lP uP assocP commP nlP nrP idemP y)
-          (FSet_ind P H eP lP uP assocP commP nlP nrP idemP z)
-  ).
-
-
-
-Axiom FSet_ind_beta_comm : forall  
-  (P : FSet -> Type)
-  (H :  forall a : FSet, IsHSet (P a))
-  (eP : P E)
-  (lP : forall a: A, P (L a))
-  (uP : forall (x y: FSet), P x -> P y -> P (U x y))
-  (assocP : forall (x y z : FSet) 
-                   (px: P x) (py: P y) (pz: P z),
-  assoc x y z #
-   (uP      x    (U y z)          px        (uP y z py pz)) 
-  = 
-   (uP   (U x y)    z       (uP x y px py)          pz))
-  (commP : forall (x y : FSet) (px: P x) (py: P y),
-  comm x y #
-  uP x y px py = uP y x py px) 
-  (nlP : forall (x : FSet) (px: P x), 
-  nl x # uP E x eP px = px)
-  (nrP : forall (x : FSet) (px: P x), 
-  nr x # uP x E px eP = px)
-  (idemP : forall (x : A), 
-  idem x # uP (L x) (L x) (lP x) (lP x) = lP x)
-  (x y : FSet),
-  apD (FSet_ind P H eP lP uP assocP commP nlP nrP idemP) (comm x y)
-  =
-  (commP x y 
-         (FSet_ind P H eP lP uP assocP commP nlP nrP idemP x)
-         (FSet_ind P H eP lP uP assocP commP nlP nrP idemP y)
-  ).
-
-Axiom FSet_ind_beta_nl : forall
-  (P : FSet -> Type)
-  (H :  forall a : FSet, IsHSet (P a))
-  (eP : P E)
-  (lP : forall a: A, P (L a))
-  (uP : forall (x y: FSet), P x -> P y -> P (U x y))
-  (assocP : forall (x y z : FSet) 
-                   (px: P x) (py: P y) (pz: P z),
-  assoc x y z #
-   (uP      x    (U y z)          px        (uP y z py pz)) 
-  = 
-   (uP   (U x y)    z       (uP x y px py)          pz))
-  (commP : forall (x y : FSet) (px: P x) (py: P y),
-  comm x y #
-  uP x y px py = uP y x py px) 
-  (nlP : forall (x : FSet) (px: P x), 
-  nl x # uP E x eP px = px)
-  (nrP : forall (x : FSet) (px: P x), 
-  nr x # uP x E px eP = px)
-  (idemP : forall (x : A), 
-  idem x # uP (L x) (L x) (lP x) (lP x) = lP x)
-  (x : FSet),
-  apD (FSet_ind P H eP lP uP assocP commP nlP nrP idemP) (nl x)
-  =
-  (nlP x (FSet_ind P H eP lP uP assocP commP nlP nrP idemP x)
-  ).
-
-Axiom FSet_ind_beta_nr : forall
-  (P : FSet -> Type)
-  (H :  forall a : FSet, IsHSet (P a))
-  (eP : P E)
-  (lP : forall a: A, P (L a))
-  (uP : forall (x y: FSet), P x -> P y -> P (U x y))
-  (assocP : forall (x y z : FSet) 
-                   (px: P x) (py: P y) (pz: P z),
-  assoc x y z #
-   (uP      x    (U y z)          px        (uP y z py pz)) 
-  = 
-   (uP   (U x y)    z       (uP x y px py)          pz))
-  (commP : forall (x y : FSet) (px: P x) (py: P y),
-  comm x y #
-  uP x y px py = uP y x py px) 
-  (nlP : forall (x : FSet) (px: P x), 
-  nl x # uP E x eP px = px)
-  (nrP : forall (x : FSet) (px: P x), 
-  nr x # uP x E px eP = px)
-  (idemP : forall (x : A), 
-  idem x # uP (L x) (L x) (lP x) (lP x) = lP x)
-  (x : FSet),
-  apD (FSet_ind P H eP lP uP assocP commP nlP nrP idemP) (nr x)
-  =
-  (nrP x (FSet_ind P H eP lP uP assocP commP nlP nrP idemP x)
-  ).
-
-Axiom FSet_ind_beta_idem : forall
-  (P : FSet -> Type)
-  (H :  forall a : FSet, IsHSet (P a))
-  (eP : P E)
-  (lP : forall a: A, P (L a))
-  (uP : forall (x y: FSet), P x -> P y -> P (U x y))
-  (assocP : forall (x y z : FSet) 
-                   (px: P x) (py: P y) (pz: P z),
-  assoc x y z #
-   (uP      x    (U y z)          px        (uP y z py pz)) 
-  = 
-   (uP   (U x y)    z       (uP x y px py)          pz))
-  (commP : forall (x y : FSet) (px: P x) (py: P y),
-  comm x y #
-  uP x y px py = uP y x py px) 
-  (nlP : forall (x : FSet) (px: P x), 
-  nl x # uP E x eP px = px)
-  (nrP : forall (x : FSet) (px: P x), 
-  nr x # uP x E px eP = px)
-  (idemP : forall (x : A), 
-  idem x # uP (L x) (L x) (lP x) (lP x) = lP x)
-  (x : A),
-  apD (FSet_ind P H eP lP uP assocP commP nlP nrP idemP) (idem x)
-  =
-  idemP x.
-
-End FSet.
-
-Instance FSet_recursion A : HitRecursion (FSet A) := {
-  indTy := _; recTy := _; 
-  H_inductor := FSet_ind A; H_recursor := FSet_rec A }.
-
-Arguments E {_}.
-Arguments U {_} _ _.
-Arguments L {_} _.
-
-End FinSet.
-
-Section functions.
-Parameter A : Type.
-Context {A_eqdec: DecidablePaths A}.
-
-Notation "{| x |}" :=  (L x).
-Infix "∪" := U (at level 8, right associativity).
-Notation "∅" := E.
-
-(** Properties of union *)
-Lemma union_idem : forall (X : FSet A), U X X = X.
-Proof.
-hinduction; try (intros; apply set_path2).
-- apply nr.
-- intros. apply idem.
-- intros X Y HX HY. etransitivity.
-  rewrite assoc. rewrite (comm _ X Y). rewrite <- (assoc _ Y X X).
-  rewrite comm.  
-  rewrite assoc. rewrite HX. rewrite HY. reflexivity.
-  rewrite comm. reflexivity.
-Defined.
-
-(** Membership predicate *)
-Definition isIn : A -> FSet A -> Bool.
-Proof.
-intros a.
-hrecursion.
-- exact false.
-- intro a'. destruct (dec (a = a')); [exact true | exact false].
-- apply orb. 
-- intros x y z. compute. destruct x; reflexivity.
-- intros x y. compute. destruct x, y; reflexivity.
-- intros x. compute. reflexivity. 
-- intros x. compute. destruct x; reflexivity.
-- intros a'. compute. destruct (A_eqdec a a'); reflexivity.
-Defined.
-
-Infix "∈" := isIn (at level 9, right associativity).
-
-Lemma isIn_singleton_eq a b : a ∈ {| b |} = true -> a = b.
-Proof. cbv.
-destruct (A_eqdec a b). intro. apply p.
-intro X. 
-contradiction (false_ne_true X).
-Defined.
-
-Lemma isIn_empty_false a : a ∈ ∅ = true -> Empty.
-Proof. 
-cbv. intro X.
-contradiction (false_ne_true X). 
-Defined.
-
-Lemma isIn_union a X Y : a ∈ (X ∪ Y) = (a ∈ X || a ∈ Y)%Bool.
-Proof. reflexivity. Qed. 
-
-(** Set comprehension *)
-Definition comprehension : 
-  (A -> Bool) -> FSet A -> FSet A.
-Proof.
-intros P.
-hrecursion.
-- apply E.
-- intro a.
-  refine (if (P a) then L a else E).
-- apply U.
-- intros. cbv. apply assoc.
-- intros. cbv. apply comm.
-- intros. cbv. apply nl.
-- intros. cbv. apply nr.
-- intros. cbv. 
-  destruct (P x); simpl.
-  + apply idem.
-  + apply nl.
-Defined.
-
-Lemma comprehension_false Y : comprehension (fun a => a ∈ ∅) Y = E.
-Proof.
-hrecursion Y; try (intros; apply set_path2).
-- cbn. reflexivity.
-- cbn. reflexivity.
-- intros x y IHa IHb.
-  cbn.
-  rewrite IHa.
-  rewrite IHb.
-  rewrite nl.
-  reflexivity.
-Defined.
-
-Lemma comprehension_union X Y Z : 
-	U (comprehension (fun a => isIn a Y) X)
-	  (comprehension (fun a => isIn a Z) X) =
-	  comprehension (fun a => isIn a (U Y Z)) X.
-Proof.
-hrecursion X; try (intros; apply set_path2).
-- cbn. apply nl.
-- cbn. intro a. 
-		destruct (isIn a Y); simpl;
-		destruct (isIn a Z); simpl.
-		apply idem.
-		apply nr.
-		apply nl.
-		apply nl.
-- cbn. intros X1 X2 IH1 IH2.
-	rewrite assoc.
-	rewrite (comm _ (comprehension (fun a : A => isIn a Y) X1) 
-				  (comprehension (fun a : A => isIn a Y) X2)).
-  rewrite <- (assoc _   
-  				  (comprehension (fun a : A => isIn a Y) X2)
-       		 (comprehension (fun a : A => isIn a Y) X1)
-       		 (comprehension (fun a : A => isIn a Z) X1)
-       		 ).
-  rewrite IH1.
-  rewrite comm.
-  rewrite assoc. 
-  rewrite (comm _ (comprehension (fun a : A => isIn a Z) X2) _).
-  rewrite IH2.
-  apply comm.
-Defined.
-
-
-Lemma comprehension_idem' `{Funext}: 
-   forall (X:FSet A), forall Y, comprehension (fun x => x ∈ (U X Y)) X = X.
-Proof.
-hinduction.
-all: try (intros; apply path_forall; intro; apply set_path2).
-- intro Y. cbv. reflexivity.
-- intros a Y. cbn.
-  destruct (dec (a = a)); simpl.
-  + reflexivity.
-  + contradiction n. reflexivity.
-- intros X1 X2 IH1 IH2 Y.
-  cbn -[isIn].
-  f_ap. 
-  + rewrite <- assoc. apply (IH1 (U X2 Y)).
-  + rewrite (comm _ X1 X2).
-    rewrite <- (assoc _ X2 X1 Y).
-    apply (IH2 (U X1 Y)).
-Defined.
-
-Lemma comprehension_idem `{Funext}: 
-   forall (X:FSet A), comprehension (fun x => x ∈ X) X = X.
-Proof.
-intros X.
-enough (comprehension (fun x : A => isIn x (U X X)) X = X).
-rewrite (union_idem) in X0. assumption.
-apply comprehension_idem'.
-Defined.
-
-(** Set intersection *)
-Definition intersection : 
-  FSet A -> FSet A -> FSet A.
-Proof.
-intros X Y.
-apply (comprehension (fun (a : A) => isIn a X) Y).
-Defined.
-
-Lemma intersection_comm X Y: intersection X Y = intersection Y X.
-Proof.
-hrecursion X;  try (intros; apply set_path2).
-- cbn. unfold intersection. apply comprehension_false.
-- cbn. unfold intersection. intros a.
-  hrecursion Y; try (intros; apply set_path2).
-  + cbn. reflexivity.
-  + cbn. intros.
-  		destruct  (dec (a0 = a)). 
-  		rewrite p. destruct (dec (a=a)).
-  		reflexivity.
-  		contradiction n. 
-  		reflexivity. 
-		destruct  (dec (a = a0)).
-		contradiction n. apply p^. reflexivity.
- 	+ cbn -[isIn]. intros Y1 Y2 IH1 IH2.
- 	 	rewrite IH1. 
- 	 	rewrite IH2. 	 	
- 	 	apply 	(comprehension_union (L a)).
-- intros X1 X2 IH1 IH2.
-  cbn.
-  unfold intersection in *.
-  rewrite <- IH1.
-  rewrite <- IH2. symmetry.
-	apply comprehension_union.
-Defined.
-
-
-(** Subset ordering *)
-Definition subset (x : FSet A) (y : FSet A) : Bool.
-Proof.
-hrecursion x.
-- apply true.
-- intro a. apply (isIn a y).
-- intros a b. apply (andb a b).
-- intros a b c. compute. destruct a; reflexivity.
-- intros a b. compute. destruct a, b; reflexivity.
-- intros x. compute. reflexivity.
-- intros x. compute. destruct x;reflexivity.
-- intros a. simpl. 
-  destruct (isIn a y); reflexivity.
-Defined.
-
-Infix "⊆" := subset (at level 8, right associativity).
-
-End functions.
\ No newline at end of file
diff --git a/FiniteSets/Enumerated.v b/FiniteSets/Enumerated.v
index d81297d..cb351f6 100644
--- a/FiniteSets/Enumerated.v
+++ b/FiniteSets/Enumerated.v
@@ -7,7 +7,7 @@ Definition Sub A := A -> hProp.
 Fixpoint listExt {A} (ls : list A) : Sub A := fun x =>
   match ls with
   | nil => False_hp
-  | cons a ls' => BuildhProp (Trunc (-1) (x = a)) \/ listExt ls' x
+  | cons a ls' => BuildhProp (Trunc (-1) (x = a)) ∨ listExt ls' x
   end.
 
 Fixpoint map {A B} (f : A -> B) (ls : list A) : list B :=
@@ -20,7 +20,7 @@ Fixpoint filterD {A} (P : A -> Bool) (ls : list A) : list { x : A | P x = true }
 Proof.
 destruct ls as [|x xs].
 - exact nil.
-- enough (P x = true \/ P x = false) as HP.
+- enough ((P x = true) + (P x = false)) as HP.
   { destruct HP as [HP | HP].
     + refine (cons (exist _ x HP) (filterD _ P xs)).
     + refine (filterD _ P xs).
@@ -55,7 +55,7 @@ Lemma filterD_lookup {A} (P : A -> Bool) (x : A) (ls : list A) (Px : P x = true)
 Proof.
 induction ls as [| a ls].
 - simpl. exact idmap.
-- assert (P a = true \/ P a = false) as HPA.
+- assert ((P a = true) + (P a = false)) as HPA.
   { destruct (P a); [left | right]; reflexivity. }
   destruct HPA as [Pa | Pa].
   + rewrite (filterD_cons P a ls Pa). simpl.
diff --git a/FiniteSets/Ext.v b/FiniteSets/Ext.v
deleted file mode 100644
index e6eb4dc..0000000
--- a/FiniteSets/Ext.v
+++ /dev/null
@@ -1,206 +0,0 @@
-(** Extensionality of the FSets *)
-Require Import HoTT HitTactics.
-Require Import definition operations.
-
-Section ext.
-Context {A : Type}.
-Context {A_deceq : DecidablePaths A}.
-
-Theorem union_idem : forall x: FSet A, U x x = x.
-Proof.
-hinduction; 
-try (intros ; apply set_path2) ; cbn.
-- apply nl.
-- apply idem.
-- intros x y P Q.
-  rewrite assoc.
-  rewrite (comm x y).
-  rewrite <- (assoc y x x).
-  rewrite P.
-  rewrite (comm y x).
-  rewrite <- (assoc x y y).
-  f_ap. 
-Defined.
-
-(** ** Properties about subset relation. *)
-Lemma subset_union `{Funext} (X Y : FSet A) : 
-  subset X Y = true -> U X Y = Y.
-Proof.
-hinduction X; try (intros; apply path_forall; intro; apply set_path2).
-- intros. apply nl.
-- intros a. hinduction Y;
-  try (intros; apply path_forall; intro; apply set_path2).
-  + intro. contradiction (false_ne_true).
-  + intros. destruct (dec (a = a0)).
-    rewrite p; apply idem.
-    contradiction (false_ne_true).
-  + intros X1 X2 IH1 IH2.
-    intro Ho.
-    destruct (isIn a X1);
-      destruct (isIn a X2).
-    * specialize (IH1 idpath).
-      rewrite assoc. f_ap. 
-    * specialize (IH1 idpath).
-      rewrite assoc. f_ap. 
-    * specialize (IH2 idpath).
-      rewrite (comm X1 X2).
-      rewrite assoc. f_ap. 
-    * contradiction (false_ne_true). 
-- intros X1 X2 IH1 IH2 G. 
-  destruct (subset X1 Y);
-    destruct (subset X2 Y).
-  * specialize (IH1 idpath).    
-    specialize (IH2 idpath).
-    rewrite <- assoc. rewrite IH2. apply IH1. 
-  * contradiction (false_ne_true).
-  * contradiction (false_ne_true).
-  * contradiction (false_ne_true).
-Defined.
-
-Lemma subset_union_l `{Funext} X :
-  forall Y, subset X (U X Y) = true.
-Proof.
-hinduction X;
-  try (intros; apply path_forall; intro; apply set_path2).
-- reflexivity.
-- intros a Y. destruct (dec (a = a)).
-  * reflexivity.
-  * by contradiction n.
-- intros X1 X2 HX1 HX2 Y.
-  refine (ap (fun z => (X1 ⊆ z && X2 ⊆ (X1 ∪ X2) ∪ Y))%Bool (assoc X1 X2 Y)^ @ _).
-  refine (ap (fun z => (X1 ⊆ _ && X2 ⊆ z ∪ Y))%Bool (comm _ _) @ _).
-  refine (ap (fun z => (X1 ⊆ _ && X2 ⊆ z))%Bool (assoc _ _ _)^ @ _).
-  rewrite HX1. simpl. apply HX2.
-Defined.
-
-Lemma subset_union_equiv `{Funext}
-  : forall X Y : FSet A, subset X Y = true <~> U X Y = Y.
-Proof.
-  intros X Y.
-  eapply equiv_iff_hprop_uncurried.
-  split.
-  -  apply subset_union.
-  - intros HXY. etransitivity.
-    apply (ap _ HXY^).
-    apply subset_union_l.
-Defined.
-
-Lemma subset_isIn `{FE : Funext} (X Y : FSet A) :
-  (forall (a : A), isIn a X = true -> isIn a Y = true)
-  <~> (subset X Y = true).
-Proof.
-  eapply equiv_iff_hprop_uncurried.
-  split.
-  - hinduction X ; try (intros ; apply path_forall ; intro ; apply set_path2).
-    + intros ; reflexivity.
-    + intros a H. 
-      apply H.
-      destruct (dec (a = a)).
-      * reflexivity.
-      * contradiction (n idpath).
-    + intros X1 X2 H1 H2 H.
-      enough (subset X1 Y = true).
-      rewrite X.
-      enough (subset X2 Y = true).
-      rewrite X0.
-      reflexivity.
-      * apply H2.
-        intros a Ha.
-        apply H.
-        rewrite Ha.
-        destruct (isIn a X1) ; reflexivity.
-      * apply H1.
-        intros a Ha.
-        apply H.
-        rewrite Ha.
-        reflexivity.        
-  - hinduction X.
-    + intros. contradiction (false_ne_true X0).
-    + intros b H a.
-      destruct (dec (a = b)).
-      * intros ; rewrite p ; apply H.
-      * intros X ; contradiction (false_ne_true X).
-    + intros X1 X2.
-      intros IH1 IH2 H1 a H2.
-      destruct (subset X1 Y) ; destruct (subset X2 Y);
-        cbv in H1; try by contradiction false_ne_true.
-      specialize (IH1 idpath a). specialize (IH2 idpath a).
-      destruct (isIn a X1); destruct (isIn a X2);
-        cbv in H2; try by contradiction false_ne_true.
-      by apply IH1.
-      by apply IH1.
-      by apply IH2.
-    + repeat (intro; intros; apply path_forall).
-      intros; intro; intros; apply set_path2.
-    + repeat (intro; intros; apply path_forall).
-      intros; intro; intros; apply set_path2.
-    + repeat (intro; intros; apply path_forall).
-      intros; intro; intros; apply set_path2.
-    + repeat (intro; intros; apply path_forall).
-      intros; intro; intros; apply set_path2.
-    + repeat (intro; intros; apply path_forall).
-      intros; intro; intros; apply set_path2.
-Defined.
-
-(** ** Extensionality proof *)
-
-Lemma eq_subset' (X Y : FSet A) : X = Y <~> (U Y X = X) * (U X Y = Y).
-Proof.
-  unshelve eapply BuildEquiv.
-  { intro H. rewrite H. split; apply union_idem. }
-  unshelve esplit.
-  { intros [H1 H2]. etransitivity. apply H1^.
-    rewrite comm. apply H2. }
-  intro; apply path_prod; apply set_path2. 
-  all: intro; apply set_path2.  
-Defined.
-
-Lemma eq_subset `{Funext} (X Y : FSet A) :
-  X = Y <~> ((subset Y X = true) * (subset X Y = true)).
-Proof.
-  transitivity ((U Y X = X) * (U X Y = Y)).
-  apply eq_subset'.
-  symmetry.
-  eapply equiv_functor_prod'; apply subset_union_equiv.
-Defined.
-
-Theorem fset_ext `{Funext} (X Y : FSet A) :
-  X = Y <~> (forall (a : A), isIn a X = isIn a Y).
-Proof.
-  etransitivity. apply eq_subset.
-  transitivity
-    ((forall a, isIn a Y = true -> isIn a X = true)
-     *(forall a, isIn a X = true -> isIn a Y = true)).
-  - eapply equiv_functor_prod';
-    apply equiv_iff_hprop_uncurried;
-    split ; apply subset_isIn.
-  - apply equiv_iff_hprop_uncurried.
-    split.
-    * intros [H1 H2 a].
-      specialize (H1 a) ; specialize (H2 a).
-      destruct (isIn a X).
-      + symmetry ; apply (H2 idpath).
-      + destruct (isIn a Y).
-        { apply (H1 idpath). }
-        { reflexivity. }
-    * intros H1.
-      split ; intro a ; intro H2.
-      + rewrite (H1 a).
-        apply H2.
-      + rewrite <- (H1 a).
-        apply H2.
-Defined.
-
-(* With extensionality we can prove decidable equality *)
-Instance fsets_dec_eq `{Funext} : DecidablePaths (FSet A).
-Proof.
-  intros X Y.
-  apply (decidable_equiv ((subset Y X = true) * (subset X Y = true)) (eq_subset X Y)^-1). (* TODO: this is so slow?*)
-  destruct (Y ⊆ X), (X ⊆ Y).
-  - left. refine (idpath, idpath).
-  - right. refine (false_ne_true o snd).
-  - right. refine (false_ne_true o fst).
-  - right. refine (false_ne_true o fst).
-Defined.
-
-End ext.
diff --git a/FiniteSets/Lattice.v b/FiniteSets/Lattice.v
index 915a041..869ea00 100644
--- a/FiniteSets/Lattice.v
+++ b/FiniteSets/Lattice.v
@@ -1,3 +1,4 @@
+(* Typeclass for lattices *)
 Require Import HoTT.
 
 Definition operation (A : Type) := A -> A -> A.
@@ -50,8 +51,8 @@ Section Lattice.
       associative_max :> Associative max ;
       idempotent_min :> Idempotent min ;
       idempotent_max :> Idempotent max ;
-      neutralL_min :> NeutralL min empty ;
-      neutralR_min :> NeutralR min empty ;
+      neutralL_min :> NeutralL max empty ;
+      neutralR_min :> NeutralR max empty ;
       absorption_min_max :> Absorption min max ;
       absorption_max_min :> Absorption max min
     }.
@@ -63,65 +64,65 @@ Arguments Lattice {_} _ _ _.
 
 Section BoolLattice.
 
-  Local Ltac solve :=
+  Ltac solve :=
     let x := fresh in
     repeat (intro x ; destruct x) 
     ; compute
     ; auto
     ; try contradiction.
 
-  Instance min_com : Commutative orb.
+  Instance orb_com : Commutative orb.
   Proof.
     solve.
   Defined.
 
-  Instance max_com : Commutative andb.
+  Instance andb_com : Commutative andb.
   Proof.
     solve.
   Defined.
 
-  Instance min_assoc : Associative orb.
+  Instance orb_assoc : Associative orb.
   Proof.
     solve.
   Defined.
 
-  Instance max_assoc : Associative andb.
+  Instance andb_assoc : Associative andb.
   Proof.
     solve.
   Defined.
 
-  Instance min_idem : Idempotent orb.
+  Instance orb_idem : Idempotent orb.
   Proof.
     solve.
   Defined.
 
-  Instance max_idem : Idempotent andb.
+  Instance andb_idem : Idempotent andb.
   Proof.
     solve.
   Defined.
 
-  Instance min_nl : NeutralL orb false.
+  Instance orb_nl : NeutralL orb false.
   Proof.
     solve.
   Defined.
 
-  Instance min_nr : NeutralR orb false.
+  Instance orb_nr : NeutralR orb false.
   Proof.
     solve.
   Defined.
 
-  Instance bool_absorption_min_max : Absorption orb andb.
+  Instance bool_absorption_orb_andb : Absorption orb andb.
   Proof.
     solve.
   Defined.
 
-  Instance bool_absorption_max_min : Absorption andb orb.
+  Instance bool_absorption_andb_orb : Absorption andb orb.
   Proof.
     solve.
   Defined.
   
-  Global Instance lattice_bool : Lattice orb andb false :=
-  { commutative_min := _ ;
+  Global Instance lattice_bool : Lattice andb orb false :=
+    { commutative_min := _ ;
       commutative_max := _ ;
       associative_min := _ ;
       associative_max := _ ;
@@ -133,9 +134,38 @@ Section BoolLattice.
       absorption_max_min := _
   }.
 
+  Definition and_true : forall b, andb b true = b.
+  Proof.
+    solve.
+  Defined.
+
+  Definition and_false : forall b, andb b false = false.
+  Proof.
+    solve.
+  Defined.
+
+  Definition dist₁ : forall b₁ b₂ b₃,
+      andb b₁ (orb b₂ b₃) = orb (andb b₁ b₂) (andb b₁ b₃).
+  Proof.
+    solve.
+  Defined.
+
+  Definition dist₂ : forall b₁ b₂ b₃,
+      orb b₁ (andb b₂ b₃) = andb (orb b₁ b₂) (orb b₁ b₃).
+  Proof.
+    solve.
+  Defined.
+
+  Definition max_min : forall b₁ b₂,
+      orb (andb b₁ b₂) b₁ = b₁.
+  Proof.
+    solve.
+  Defined.
+  
 End BoolLattice.
 
 Hint Resolve
-     min_com max_com min_assoc max_assoc min_idem max_idem min_nl min_nr
-     bool_absorption_min_max bool_absorption_max_min
+     orb_com andb_com orb_assoc andb_assoc orb_idem andb_idem orb_nl orb_nr
+     bool_absorption_orb_andb bool_absorption_andb_orb and_true and_false
+     dist₁ dist₂ max_min
  : bool_lattice_hints.
diff --git a/FiniteSets/Lists.v b/FiniteSets/Lists.v
index 2d8f11a..b331126 100644
--- a/FiniteSets/Lists.v
+++ b/FiniteSets/Lists.v
@@ -1,5 +1,5 @@
 Require Import HoTT HitTactics.
-Require Import cons_repr operations definition.
+Require Import cons_repr operations_decidable properties_decidable definition.
 
 Section Operations.
   Variable A : Type.
@@ -43,11 +43,10 @@ Arguments append {_} _ _.
 Arguments empty {_}.
 Arguments filter {_} _ _.
 Arguments cardinality {_} {_} _.
-Arguments intersection {_} {_} _ _.
 
 Section ListToSet.
   Variable A : Type.
-  Context {A_deceq : DecidablePaths A} `{Funext}.
+  Context {A_deceq : DecidablePaths A} `{Univalence}.
   
   Fixpoint list_to_setC (l : list A) : FSetC A :=
     match l with
@@ -71,13 +70,13 @@ Section ListToSet.
   Defined.
 
   Lemma member_isIn (l : list A) (a : A) :
-    member l a = isIn a (FSetC_to_FSet (list_to_setC l)).
+    member l a = isIn_b a (FSetC_to_FSet (list_to_setC l)).
   Proof.
     induction l ; cbn in *.
     - reflexivity.
     - destruct (dec (a = a0)) ; cbn.
-      * reflexivity.
-      * apply IHl.
+      * rewrite ?p. simplify_isIn. reflexivity.
+      * rewrite IHl. simplify_isIn. rewrite L_isIn_b_false ; auto.
   Defined.
 
   Lemma append_FSetCappend (l1 l2 : list A) :
diff --git a/FiniteSets/_CoqProject b/FiniteSets/_CoqProject
index 438e7d5..f9a23eb 100644
--- a/FiniteSets/_CoqProject
+++ b/FiniteSets/_CoqProject
@@ -1,15 +1,17 @@
 -R . "" COQC = hoqc COQDEP = hoqdep
 -R ../prelude ""
-definition.v
+lattice.v
 disjunction.v
-operations.v
-Ext.v
-properties.v
-empty_set.v
-ordered.v
-cons_repr.v
-Lattice.v
-monad.v
-Lists.v
 bad.v
+definition.v
+operations.v
+properties.v
+operations_decidable.v
+extensionality.v
+properties_decidable.v
+monad.v
+cons_repr.v
+lists.v
 Enumerated.v
+#empty_set.v
+#ordered.v
diff --git a/FiniteSets/cons_repr.v b/FiniteSets/cons_repr.v
index db8672b..d3fec87 100644
--- a/FiniteSets/cons_repr.v
+++ b/FiniteSets/cons_repr.v
@@ -1,10 +1,5 @@
-Require Import HoTT.
-Require Import HitTactics.
-Require Import definition.
-Require Import operations.
-Require Import properties.
-Require Import empty_set.
-
+Require Import HoTT HitTactics.
+Require Import definition operations_decidable properties_decidable.
 
 Module Export FSetC.
  
@@ -295,25 +290,25 @@ Section Length.
 
 Context {A : Type}.
 Context {A_deceq : DecidablePaths A}.
-Context {H : Funext}.
+Context `{Univalence}.
 
+Opaque isIn_b.
 Definition length (x: FSetC A) : nat.
 Proof.
 simple refine (FSetC_ind A _ _ _ _ _ _ x ); simpl.
 - exact 0.
 - intros a y n. 
   pose (y' := FSetC_to_FSet y).
-  exact (if isIn a y' then n else (S n)).
-- intros. rewrite transport_const. cbn. 
-  destruct (dec (a = a)); cbn. reflexivity.
-  destruct n; reflexivity.
+  exact (if isIn_b a y' then n else (S n)).
 - intros. rewrite transport_const. cbn.
-  destruct (dec (a = b)), (dec (b = a)); cbn. 
-  + rewrite p. reflexivity.
-  + contradiction (n p^).
-  + contradiction (n p^).
-  + intros. 
-  destruct (a ∈ (FSetC_to_FSet x0)), (b ∈ (FSetC_to_FSet x0)); reflexivity.
+  simplify_isIn. simpl. reflexivity.
+- intros. rewrite transport_const. cbn.
+  simplify_isIn.
+  destruct (dec (a = b)) as [Hab | Hab].
+  + rewrite Hab. simplify_isIn. simpl. reflexivity.
+  + rewrite ?L_isIn_b_false; auto. simpl. 
+    destruct (isIn_b a (FSetC_to_FSet x0)), (isIn_b b (FSetC_to_FSet x0)) ; reflexivity.
+    intro p. contradiction (Hab p^).
 Defined.
 
 Definition length_FSet (x: FSet A) := length (FSet_to_FSetC x).
@@ -325,8 +320,3 @@ cbn. reflexivity.
 Defined.
 
 End Length.
-
-
-
-
-
diff --git a/FiniteSets/definition.v b/FiniteSets/definition.v
index ecdd2e3..ea167b4 100644
--- a/FiniteSets/definition.v
+++ b/FiniteSets/definition.v
@@ -1,3 +1,4 @@
+(* Definitions of the Kuratowski-finite sets via a HIT *)
 Require Import HoTT.
 Require Import HitTactics.
 
@@ -72,11 +73,9 @@ Fixpoint FSet_ind
   {struct x}
   : P x
   := (match x return _ -> _ -> _ -> _ -> _ -> _ -> P x with
-        | E => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => eP
-        | L a => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => lP a
-        | U y z => fun _ => fun _ => fun _ => fun _ => fun _ => fun _ => uP y z
-           (FSet_ind y)
-           (FSet_ind z)
+      | E => fun _ _ _ _ _ _ => eP
+      | L a => fun _ _ _ _ _ _ => lP a
+      | U y z => fun _ _ _ _ _ _ => uP y z (FSet_ind y) (FSet_ind z)
       end) H assocP commP nlP nrP idemP.
 
 
diff --git a/FiniteSets/disjunction.v b/FiniteSets/disjunction.v
index 55a02a3..0a99ffb 100644
--- a/FiniteSets/disjunction.v
+++ b/FiniteSets/disjunction.v
@@ -1,14 +1,18 @@
+(* Logical disjunction in HoTT (see ch. 3 of the book) *)
 Require Import HoTT.
 
 Definition lor (X Y : hProp) : hProp := BuildhProp (Trunc (-1) (sum X Y)).
 
-Infix "\/" := lor.
+Delimit Scope logic_scope with L.
+Notation "A ∨ B" := (lor A B) (at level 20, right associativity) : logic_scope.
+Arguments lor _%L _%L.
+Open Scope logic_scope.
 
-Section lor_props.
+Section lor_props. 
   Variable X Y Z : hProp.
   Context `{Univalence}.
-
-  Theorem lor_assoc : (X \/ (Y \/ Z)) = ((X \/ Y) \/ Z).
+  
+  Theorem lor_assoc : X ∨ Y ∨ Z = (X ∨ Y) ∨ Z.
   Proof.
     apply path_iff_hprop ; cbn.
     * simple refine (Trunc_ind _ _).
@@ -27,7 +31,7 @@ Section lor_props.
       + apply (tr (inr (tr (inr z)))).
   Defined.
 
-  Theorem lor_comm : (X \/ Y) = (Y \/ X).
+  Theorem lor_comm : X ∨ Y = Y ∨ X.
   Proof.
     apply path_iff_hprop ; cbn.
     * simple refine (Trunc_ind _ _).
@@ -40,7 +44,7 @@ Section lor_props.
       + apply (tr (inl x)).
   Defined.
 
-  Theorem lor_nl : (False_hp \/ X) = X.
+  Theorem lor_nl : False_hp ∨ X = X.
   Proof.
     apply path_iff_hprop ; cbn.
     * simple refine (Trunc_ind _ _).
@@ -50,7 +54,7 @@ Section lor_props.
     * apply (fun x => tr (inr x)).
   Defined.
 
-  Theorem lor_nr : (X \/ False_hp) = X.
+  Theorem lor_nr : X ∨ False_hp = X.
   Proof.
     apply path_iff_hprop ; cbn.
     * simple refine (Trunc_ind _ _).
@@ -60,7 +64,7 @@ Section lor_props.
     * apply (fun x => tr (inl x)).
   Defined.
 
-  Theorem lor_idem : (X \/ X) = X.
+  Theorem lor_idem : X ∨ X = X.
   Proof.
     apply path_iff_hprop ; cbn.
     - simple refine (Trunc_ind _ _).
diff --git a/FiniteSets/extensionality.v b/FiniteSets/extensionality.v
new file mode 100644
index 0000000..89237a3
--- /dev/null
+++ b/FiniteSets/extensionality.v
@@ -0,0 +1,110 @@
+(** Extensionality of the FSets *)
+Require Import HoTT HitTactics.
+Require Import definition operations properties.
+
+Section ext.
+Context {A : Type}.
+Context `{Univalence}.
+
+Lemma subset_union_equiv
+  : forall X Y : FSet A, subset X Y <~> U X Y = Y.
+Proof.
+  intros X Y.
+  eapply equiv_iff_hprop_uncurried.
+  split.
+  - apply subset_union.
+  - intro HXY.
+    rewrite <- HXY.
+    apply subset_union_l.
+Defined.
+
+Lemma subset_isIn (X Y : FSet A) :
+  (forall (a : A), isIn a X -> isIn a Y)
+  <~> (subset X Y).
+Proof.
+  eapply equiv_iff_hprop_uncurried.
+  split.
+  - hinduction X ;
+      try (intros; repeat (apply path_forall; intro); apply equiv_hprop_allpath ; apply _).
+    + intros ; reflexivity.
+    + intros a f.
+      apply f.
+      apply tr ; reflexivity.
+    + intros X1 X2 H1 H2 f.
+      enough (subset X1 Y).
+      enough (subset X2 Y).
+      { split. apply X. apply X0. }
+      * apply H2.
+        intros a Ha.
+        apply f.
+        apply tr.
+        right.
+        apply Ha.
+      * apply H1.
+        intros a Ha.
+        apply f.
+        apply tr.
+        left.
+        apply Ha.
+  - hinduction X ;
+      try (intros; repeat (apply path_forall; intro); apply equiv_hprop_allpath ; apply _).
+    + intros. contradiction.
+    + intros b f a.
+      simple refine (Trunc_ind _ _) ; cbn.
+      intro p.
+      rewrite p^ in f.
+      apply f.
+    + intros X1 X2 IH1 IH2 [H1 H2] a.
+      simple refine (Trunc_ind _ _) ; cbn.
+      intros [C1 | C2].
+      ++ apply (IH1 H1 a C1).
+      ++ apply (IH2 H2 a C2).
+Defined.
+
+(** ** Extensionality proof *)
+
+Lemma eq_subset' (X Y : FSet A) : X = Y <~> (U Y X = X) * (U X Y = Y).
+Proof.
+  unshelve eapply BuildEquiv.
+  { intro H'. rewrite H'. split; apply union_idem. }
+  unshelve esplit.
+  { intros [H1 H2]. etransitivity. apply H1^.
+    rewrite comm. apply H2. }
+  intro; apply path_prod; apply set_path2. 
+  all: intro; apply set_path2.  
+Defined.
+
+Lemma eq_subset (X Y : FSet A) :
+  X = Y <~> (subset Y X * subset X Y).
+Proof.
+  transitivity ((U Y X = X) * (U X Y = Y)).
+  apply eq_subset'.
+  symmetry.
+  eapply equiv_functor_prod'; apply subset_union_equiv.
+Defined.
+
+Theorem fset_ext (X Y : FSet A) :
+  X = Y <~> (forall (a : A), isIn a X = isIn a Y).
+Proof.
+  refine (@equiv_compose' _ _ _ _ _) ; [ | apply eq_subset ].
+  refine (@equiv_compose' _ ((forall a, isIn a Y -> isIn a X)
+                             *(forall a, isIn a X -> isIn a Y)) _ _ _).
+  - apply equiv_iff_hprop_uncurried.
+    split.
+    * intros [H1 H2 a].
+      specialize (H1 a) ; specialize (H2 a).
+      apply path_iff_hprop.
+      apply H2.
+      apply H1.
+    * intros H1.
+      split ; intro a ; intro H2.
+      + rewrite (H1 a).
+        apply H2.
+      + rewrite <- (H1 a).
+        apply H2.
+  - eapply equiv_functor_prod' ;
+    apply equiv_iff_hprop_uncurried ;
+    split ; apply subset_isIn.
+Defined.
+
+End ext.
diff --git a/FiniteSets/monad.v b/FiniteSets/monad.v
index 7e7ecf1..0a06e5a 100644
--- a/FiniteSets/monad.v
+++ b/FiniteSets/monad.v
@@ -1,6 +1,6 @@
 (* [FSet] is a (strong and stable) finite powerset monad *)
-Require Export definition properties.
 Require Import HoTT HitTactics.
+Require Export definition properties.
 
 Definition ffmap {A B : Type} : (A -> B) -> FSet A -> FSet B.
 Proof.
@@ -19,7 +19,7 @@ Defined.
 Lemma ffmap_1 `{Funext} {A : Type} : @ffmap A A idmap = idmap.
 Proof.
   apply path_forall.
-  intro x. hinduction x; try (cbn; intros; f_ap);
+  intro x. hinduction x; try (intros; f_ap);
              try (intros; apply set_path2).
 Defined.
 
@@ -30,7 +30,7 @@ Lemma ffmap_compose {A B C : Type} `{Funext} (f : A -> B) (g : B -> C) :
   fmap FSet (g o f) = fmap _ g o fmap _ f.
 Proof.
   apply path_forall. intro x.
-  hrecursion x; try (cbn; intros; f_ap);
+  hrecursion x; try (intros; f_ap);
     try (intros; apply set_path2).
 Defined.
 
@@ -50,7 +50,7 @@ Defined.
 Lemma join_assoc {A : Type} (X : FSet (FSet (FSet A))) :
   join (ffmap join X) = join (join X).
 Proof.
-  hrecursion X; try (cbn; intros; f_ap);
+  hrecursion X; try (intros; f_ap);
     try (intros; apply set_path2).
 Defined.
 
@@ -61,7 +61,7 @@ Proof. reflexivity. Defined.
 Lemma join_return_fmap {A : Type} (X : FSet A) :
   join ({| X |}) = join (ffmap (fun x => {|x|}) X).
 Proof.
-  hrecursion X; try (cbn; intros; f_ap);
+  hrecursion X; try (intros; f_ap);
     try (intros; apply set_path2).
 Defined.
 
diff --git a/FiniteSets/operations.v b/FiniteSets/operations.v
index 9f46115..838a9e6 100644
--- a/FiniteSets/operations.v
+++ b/FiniteSets/operations.v
@@ -1,28 +1,53 @@
+(* Operations on the [FSet A] for an arbitrary [A] *)
 Require Import HoTT HitTactics.
-Require Import definition.
+Require Import definition disjunction lattice.
+
 Section operations.
-
 Context {A : Type}.
-Context {A_deceq : DecidablePaths A}.
+Context `{Univalence}.
 
-Definition isIn : A -> FSet A -> Bool.
+Definition isIn : A -> FSet A -> hProp.
 Proof.
 intros a.
 hrecursion.
-- exact false.
-- intro a'. destruct (dec (a = a')); [exact true | exact false].
-- apply orb. 
-- intros x y z. compute. destruct x; reflexivity.
-- intros x y. compute. destruct x, y; reflexivity.
-- intros x. compute. reflexivity. 
-- intros x. compute. destruct x; reflexivity.
-- intros a'. simpl.
-  destruct (match dec (a = a') with
-  | inl _ => true
-  | inr _ => false
-  end); compute; reflexivity. 
+- exists Empty.
+  exact _.
+- intro a'.
+  exists (Trunc (-1) (a = a')).
+  exact _.
+- apply lor. 
+- intros ; apply lor_assoc. exact _.
+- intros ; apply lor_comm. exact _.
+- intros ; apply lor_nl. exact _.
+- intros ; apply lor_nr. exact _.
+- intros ; apply lor_idem. exact _.
 Defined.
 
+Definition subset : FSet A -> FSet A -> hProp.
+Proof.
+intros X Y.
+hrecursion X.
+- exists Unit.
+  exact _.
+- intros a.
+  apply (isIn a Y).
+- intros X1 X2.
+  exists (prod X1 X2).
+  exact _.
+- intros.
+  apply path_trunctype ; apply equiv_prod_assoc.
+- intros.
+  apply path_trunctype ; apply equiv_prod_symm.
+- intros.
+  apply path_trunctype ; apply prod_unit_l.
+- intros.
+  apply path_trunctype ; apply prod_unit_r.
+- intros a'.
+  apply path_iff_hprop ; cbn.
+  * intros [p1 p2]. apply p1.
+  * intros p.
+    split ; apply p.
+Defined.
 
 Definition comprehension : 
   (A -> Bool) -> FSet A -> FSet A.
@@ -33,43 +58,31 @@ hrecursion.
 - intro a.
   refine (if (P a) then L a else E).
 - apply U.
-- intros. cbv. apply assoc.
-- intros. cbv. apply comm.
-- intros. cbv. apply nl.
-- intros. cbv. apply nr.
-- intros. cbv. 
-  destruct (P x); simpl.
+- apply assoc.
+- apply comm.
+- apply nl.
+- apply nr.
+- intros; simpl. 
+  destruct (P x).
   + apply idem.
   + apply nl.
 Defined.
 
-Definition intersection : 
-  FSet A -> FSet A -> FSet A.
+Definition isEmpty :
+  FSet A -> Bool.
 Proof.
-intros X Y.
-apply (comprehension (fun (a : A) => isIn a X) Y).
-Defined.
-
-Definition difference :
-  FSet A -> FSet A -> FSet A := fun X Y =>
-  comprehension (fun a => negb (isIn a X)) Y.
-
-Definition subset :
-	FSet A -> FSet A -> Bool.
-Proof.
-intros X Y.
-hrecursion X. 
-- exact true.
-- exact (fun a => (isIn a Y)).
-- exact andb.
-- intros. compute. destruct x; reflexivity.
-- intros x y; compute; destruct x, y; reflexivity. 
-- intros x; compute; destruct x; reflexivity.
-- intros x; compute; destruct x; reflexivity.
-- intros x; cbn; destruct (isIn x Y); reflexivity.
-Defined.
-
+  hrecursion.
+  - apply true.
+  - apply (fun _ => false).
+  - apply andb.
+  - intros. symmetry. eauto with bool_lattice_hints.
+  - eauto with bool_lattice_hints.
+  - eauto with bool_lattice_hints.
+  - eauto with bool_lattice_hints.
+  - eauto with bool_lattice_hints.
+Defined.    
+  
 End operations.
 
 Infix "∈" := isIn (at level 9, right associativity).
-Infix  "⊆" := subset (at level 10, right associativity).
+Infix  "⊆" := subset (at level 10, right associativity).
\ No newline at end of file
diff --git a/FiniteSets/operations_decidable.v b/FiniteSets/operations_decidable.v
new file mode 100644
index 0000000..bdc6e70
--- /dev/null
+++ b/FiniteSets/operations_decidable.v
@@ -0,0 +1,41 @@
+(* Operations on [FSet A] when [A] has decidable equality *)
+Require Import HoTT HitTactics.
+Require Export definition operations.
+
+Section decidable_A.
+  Context {A : Type}.
+  Context {A_deceq : DecidablePaths A}.
+  Context `{Univalence}.
+
+  Global Instance isIn_decidable : forall (a : A) (X : FSet A), Decidable (isIn a X).
+  Proof.
+    intros a.
+    hinduction ; try (intros ; apply path_ishprop).
+    - apply _.
+    - intros. apply _.
+    - intros. apply _. 
+  Defined.
+
+  Definition isIn_b (a : A) (X : FSet A) :=
+    match dec (isIn a X) with
+    | inl _ => true
+    | inr _ => false
+    end.
+  
+  Global Instance subset_decidable : forall (X Y : FSet A), Decidable (subset X Y).
+  Proof.
+    hinduction ; try (intros ; apply path_ishprop).
+    - intro ; apply _.
+    - intros ; apply _. 
+    - intros ; apply _.
+  Defined.
+
+  Definition subset_b (X Y : FSet A) :=
+    match dec (subset X Y) with
+    | inl _ => true
+    | inr _ => false
+    end.
+
+  Definition intersection (X Y : FSet A) : FSet A := comprehension (fun a => isIn_b a Y) X. 
+
+End decidable_A.
\ No newline at end of file
diff --git a/FiniteSets/properties.v b/FiniteSets/properties.v
index 24c293d..6aa679f 100644
--- a/FiniteSets/properties.v
+++ b/FiniteSets/properties.v
@@ -1,68 +1,82 @@
 Require Import HoTT HitTactics.
-Require Export definition operations Ext Lattice.
+Require Export definition operations disjunction.
 
 (* Lemmas relating operations to the membership predicate *)
 Section operations_isIn.
 
-Context {A : Type} `{DecidablePaths A}.
+Context {A : Type}.
+Context `{Univalence}.
 
-Lemma ext `{Funext}  : forall (S T : FSet A), (forall a, isIn a S = isIn a T) -> S = T.
+
+
+Lemma union_idem : forall x: FSet A, U x x = x.
 Proof.
-  apply fset_ext.
+hinduction; 
+try (intros ; apply set_path2) ; cbn.
+- apply nl.
+- apply idem.
+- intros x y P Q.
+  rewrite assoc.
+  rewrite (comm x y).
+  rewrite <- (assoc y x x).
+  rewrite P.
+  rewrite (comm y x).
+  rewrite <- (assoc x y y).
+  f_ap. 
+Defined.
+
+(** ** Properties about subset relation. *)
+Lemma subset_union (X Y : FSet A) : 
+  subset X Y -> U X Y = Y.
+Proof.
+hinduction X; try (intros; apply path_forall; intro; apply set_path2).
+- intros. apply nl.
+- intros a. hinduction Y;
+  try (intros; apply path_forall; intro; apply set_path2).
+  + intro.
+    contradiction.
+  + intro a0.
+    simple refine (Trunc_ind _ _).
+    intro p ; cbn. 
+    rewrite p; apply idem.
+  + intros X1 X2 IH1 IH2.
+    simple refine (Trunc_ind _ _).
+    intros [e1 | e2].
+    ++ rewrite assoc.
+       rewrite (IH1 e1).
+       reflexivity.
+    ++ rewrite comm.
+       rewrite <- assoc.
+       rewrite (comm X2).
+       rewrite (IH2 e2).
+       reflexivity.
+- intros X1 X2 IH1 IH2 [G1 G2].
+  rewrite <- assoc.
+  rewrite (IH2 G2).
+  apply (IH1 G1).
+Defined.
+
+Lemma subset_union_l (X : FSet A) :
+  forall Y, subset X (U X Y).
+Proof.
+hinduction X ;
+  try (repeat (intro; intros; apply path_forall); intro; apply equiv_hprop_allpath ; apply _).
+- apply (fun _ => tt).
+- intros a Y.
+  apply tr ; left ; apply tr ; reflexivity.
+- intros X1 X2 HX1 HX2 Y.
+  split. 
+  * rewrite <- assoc. apply HX1.
+  * rewrite (comm X1 X2). rewrite <- assoc. apply HX2.
 Defined.
 
 (* Union and membership *)
 Lemma union_isIn (X Y : FSet A) (a : A) :
-  isIn a (U X Y) = orb (isIn a X) (isIn a Y).
+  isIn a (U X Y) = isIn a X ∨ isIn a Y.
 Proof.
   reflexivity.
 Defined.
 
-(* Intersection and membership. We need a bunch of supporting lemmas *)
-Lemma intersection_0l: forall X: FSet A, intersection E X = E.
-Proof.
-hinduction; 
-try (intros ; apply set_path2).
-- reflexivity.
-- intro a.
-  reflexivity.
-- intros x y P Q.
-  cbn.
-  rewrite P.
-  rewrite Q.
-  apply union_idem.
-Defined.
-
-Lemma intersection_0r (X : FSet A) : intersection X E = E.
-Proof.
-  exact idpath.
-Defined.
-
-Lemma intersection_La (X : FSet A) (a : A) :
-    intersection (L a) X = if isIn a X then L a else E.
-Proof.
-hinduction X; try (intros ; apply set_path2).
-- reflexivity.
-- intro b.
-  cbn.
-  destruct (dec (a = b)) as [p|np].
-  * rewrite p.
-    destruct (dec (b = b)) as [|nb]; [reflexivity|].
-    by contradiction nb.
-  * destruct (dec (b = a)); [|reflexivity].
-    by contradiction np.
-- unfold intersection.
-  intros X Y P Q.
-  cbn.
-  rewrite P.
-  rewrite Q.
-  destruct (isIn a X) ; destruct (isIn a Y).
-  * apply union_idem.
-  * apply nr.
-  * apply nl. 
-  * apply union_idem.
-Defined.
-
 Lemma comprehension_or : forall ϕ ψ (x: FSet A),
     comprehension (fun a => orb (ϕ a) (ψ a)) x = U (comprehension ϕ x) 
     (comprehension ψ x).
@@ -87,174 +101,23 @@ hinduction; try (intros; apply set_path2).
   reflexivity.
 Defined.
 
-Lemma distributive_La (z : FSet A) (a : A) : forall Y : FSet A, 
-       intersection (U (L a) z) Y = U (intersection (L a) Y) (intersection z Y).
-Proof.
-hinduction; try (intros ; apply set_path2) ; cbn.
-- symmetry ; apply nl.
-- intros b.
-  destruct (dec (b = a)) ; cbn.
-  * destruct (isIn b z).
-    + rewrite union_idem.
-      reflexivity.
-    + rewrite nr.
-      reflexivity.
-  * rewrite nl ; reflexivity.
-- intros X1 X2 P Q.
-  rewrite P. rewrite Q.
-  rewrite <- assoc.
-  rewrite (comm (comprehension (fun a0 : A => isIn a0 z) X1)).
-  rewrite <- assoc.
-  rewrite assoc.
-  rewrite (comm (comprehension (fun a0 : A => isIn a0 z) X2)).
-  reflexivity.
-Defined.
-
-Lemma distributive_intersection_U (X1 X2 Y : FSet A) :
-    intersection (U X1 X2) Y = U (intersection X1 Y) (intersection X2 Y).
-Proof.
-hinduction X1; try (intros ; apply set_path2) ; cbn.
-- rewrite intersection_0l.
-  rewrite nl.
-  rewrite nl.
-  reflexivity.
-- intro a.
-  rewrite intersection_La.
-  rewrite distributive_La.
-  rewrite intersection_La.
-  reflexivity.
-- intros Z1 Z2 P Q.
-  unfold intersection in *. simpl in *.
-  apply comprehension_or.
-Defined.
-
-Theorem intersection_isIn (X Y: FSet A) (a : A) :
-    isIn a (intersection X Y) = andb (isIn a X) (isIn a Y).
-Proof.
-hinduction X; try (intros ; apply set_path2) ; cbn.
-- rewrite intersection_0l.
-  reflexivity.
-- intro b.
-  rewrite intersection_La.
-  destruct (dec (a = b)) ; cbn.
-  * rewrite p.
-    destruct (isIn b Y).
-    + cbn.
-      destruct (dec (b = b)); [reflexivity|].
-      by contradiction n.
-    + reflexivity.
-  * destruct (isIn b Y).
-    + cbn.
-      destruct (dec (a = b)); [|reflexivity].
-      by contradiction n.
-    + reflexivity.
-- intros X1 X2 P Q.
-  rewrite distributive_intersection_U. simpl.
-  rewrite P.
-  rewrite Q.
-  destruct (isIn a X1) ; destruct (isIn a X2) ; destruct (isIn a Y) ; 
-  reflexivity.
-Defined.
 End operations_isIn.
 
-(* Some suporting tactics *)
-Ltac simplify_isIn :=
-  repeat (rewrite ?intersection_isIn ;
-          rewrite ?union_isIn).
-  
-Ltac toBool := try (intro) ;
-    intros ; apply ext ; intros ; simplify_isIn ; eauto with bool_lattice_hints.
-
-Section SetLattice.
-
-  Context {A : Type}.
-  Context {A_deceq : DecidablePaths A}.
-  Context `{Funext}.
-
-  Instance fset_union_com : Commutative (@U A).
-  Proof. 
-    toBool.
-  Defined.
-
-  Instance fset_intersection_com : Commutative intersection.
-  Proof.
-    toBool.
-  Defined.
-
-  Instance fset_union_assoc : Associative (@U A).
-  Proof.
-    toBool.
-  Defined.
-
-  Instance fset_intersection_assoc : Associative intersection.
-  Proof.
-    toBool.
-  Defined.
-
-  Instance fset_union_idem : Idempotent (@U A).
-  Proof. exact union_idem. Defined.
-
-  Instance fset_intersection_idem : Idempotent intersection.
-  Proof.
-    toBool.
-  Defined.
-
-  Instance fset_union_nl : NeutralL (@U A) (@E A).
-  Proof.
-    toBool.
-  Defined.
-
-  Instance fset_union_nr : NeutralR (@U A) (@E A).
-  Proof.
-    toBool.
-  Defined.
-
-  Instance fset_absorption_intersection_union : Absorption (@U A) intersection.
-  Proof.
-    toBool.
-  Defined.
-
-  Instance fset_absorption_union_intersection : Absorption intersection (@U A).
-  Proof.
-    toBool.
-  Defined.
-  
-  Instance lattice_fset : Lattice (@U A) intersection (@E A) :=
-    {
-      commutative_min := _ ;
-      commutative_max := _ ;
-      associative_min := _ ;
-      associative_max := _ ;
-      idempotent_min := _ ;
-      idempotent_max := _ ;
-      neutralL_min := _ ;
-      neutralR_min := _ ;
-      absorption_min_max := _ ;
-      absorption_max_min := _
-    }.
-
-End SetLattice.
-
 (* Other properties *)
 Section properties.
 
 Context {A : Type}.
-Context {A_deceq : DecidablePaths A}.
+Context `{Univalence}.
 
 (** isIn properties *)
-Lemma singleton_isIn (a b: A) : isIn a  (L b) = true -> a = b.
+Lemma singleton_isIn (a b: A) : isIn a (L b) -> Trunc (-1) (a = b).
 Proof.
-  simpl. 
-  destruct (dec (a = b)).
-  - intro.
-    apply p.
-  - intro X. 
-    contradiction (false_ne_true X).
+  apply idmap.
 Defined.
 
-Lemma empty_isIn (a: A) : isIn a E = false.
+Lemma empty_isIn (a: A) : isIn a E -> Empty.
 Proof. 
-  reflexivity.
+  apply idmap.
 Defined.
 
 (** comprehension properties *)
@@ -269,7 +132,7 @@ hrecursion Y; try (intros; apply set_path2).
   apply union_idem.
 Defined.
 
-Theorem comprehension_subset : forall ϕ (X : FSet A),
+Lemma comprehension_subset : forall ϕ (X : FSet A),
     U (comprehension ϕ X) X = X.
 Proof.
 intros ϕ.
@@ -290,29 +153,4 @@ hrecursion; try (intros ; apply set_path2) ; cbn.
   reflexivity.
 Defined.
 
-Theorem comprehension_all : forall (X : FSet A),
-    comprehension (fun a => isIn a X) X = X.
-Proof.
-hinduction; try (intros ; apply set_path2).
-- reflexivity.
-- intro a.
-  destruct (dec (a = a)).
-  * reflexivity.
-  * contradiction (n idpath).
-- intros X1 X2 P Q.
-  f_ap; (etransitivity; [ apply comprehension_or |]).
-  rewrite P. rewrite (comm X1).
-  apply comprehension_subset.
-
-  rewrite Q.
-  apply comprehension_subset.
-Defined.
-  
-Theorem distributive_U_int `{Funext} (X1 X2 Y : FSet A) :
-    U (intersection X1 X2) Y = intersection (U X1 Y) (U X2 Y).
-Proof.
-  toBool.
-  destruct (a ∈ X1), (a ∈ X2), (a ∈ Y); eauto.
-Defined.
-
 End properties.
diff --git a/FiniteSets/properties_decidable.v b/FiniteSets/properties_decidable.v
new file mode 100644
index 0000000..ffdd3ba
--- /dev/null
+++ b/FiniteSets/properties_decidable.v
@@ -0,0 +1,276 @@
+(* Properties of [FSet A] where [A] has decidable equality *)
+Require Import HoTT HitTactics.
+Require Export properties extensionality lattice operations_decidable.
+
+(* Lemmas relating operations to the membership predicate *)
+Section operations_isIn.
+
+Context {A : Type} `{DecidablePaths A} `{Univalence}.
+
+Lemma ext : forall (S T : FSet A), (forall a, isIn_b a S = isIn_b a T) -> S = T.
+Proof.
+  intros X Y H2.
+  apply fset_ext.
+  intro a.
+  specialize (H2 a).
+  unfold isIn_b, dec in H2.
+  destruct (isIn_decidable a X) ; destruct (isIn_decidable a Y).
+  - apply path_iff_hprop ; intro ; assumption.
+  - contradiction (true_ne_false).
+  - contradiction (true_ne_false) ; apply H2^.
+  - apply path_iff_hprop ; intro ; contradiction.
+Defined.
+
+Lemma empty_isIn (a : A) :
+  isIn_b a ∅ = false.
+Proof.
+  reflexivity.
+Defined.
+
+Lemma L_isIn (a b : A) :
+  isIn a {|b|} -> a = b.
+Proof.
+  intros. strip_truncations. assumption.
+Defined.
+
+Lemma L_isIn_b_true (a b : A) (p : a = b) :
+  isIn_b a {|b|} = true.
+Proof.
+  unfold isIn_b, dec.
+  destruct (isIn_decidable a {|b|}) as [n | n] .
+  - reflexivity.
+  - simpl in n.
+    contradiction (n (tr p)).
+Defined.
+
+Lemma L_isIn_b_aa (a : A) :
+  isIn_b a {|a|} = true.
+Proof.
+  apply L_isIn_b_true ; reflexivity.
+Defined.
+
+Lemma L_isIn_b_false (a b : A) (p : a <> b) :
+  isIn_b a {|b|} = false.
+Proof.
+  unfold isIn_b, dec.
+  destruct (isIn_decidable a {|b|}).
+  - simpl in t.
+    strip_truncations.
+    contradiction.
+  - reflexivity.
+Defined.
+    
+(* Union and membership *)
+Lemma union_isIn (X Y : FSet A) (a : A) :
+  isIn_b a (U X Y) = orb (isIn_b a X) (isIn_b a Y).
+Proof.
+  unfold isIn_b ; unfold dec.
+  simpl.
+  destruct (isIn_decidable a X) ; destruct (isIn_decidable a Y) ; reflexivity.
+Defined.
+
+Lemma intersection_isIn (X Y: FSet A) (a : A) :
+    isIn_b a (intersection X Y) = andb (isIn_b a X) (isIn_b a Y).
+Proof.
+  hinduction X; try (intros ; apply set_path2).
+  - reflexivity.
+  - intro b.
+    destruct (dec (a = b)).
+    * rewrite p.
+      destruct (isIn_b b Y) ; symmetry ; eauto with bool_lattice_hints.
+    * destruct (isIn_b b Y) ; destruct (isIn_b a Y) ; symmetry ; eauto with bool_lattice_hints.
+      + rewrite and_false.
+        symmetry.
+        apply (L_isIn_b_false a b n).
+      + rewrite and_true.
+        apply (L_isIn_b_false a b n).
+  - intros X1 X2 P Q.
+    rewrite union_isIn ; rewrite union_isIn.
+    rewrite P.
+    rewrite Q.
+    unfold isIn_b, dec.
+    destruct (isIn_decidable a X1)
+    ; destruct (isIn_decidable a X2)
+    ; destruct (isIn_decidable a Y)
+    ; reflexivity.
+Defined.
+
+Lemma comprehension_isIn (Y : FSet A) (ϕ : A -> Bool) (a : A) :
+  isIn_b a (comprehension ϕ Y) = andb (isIn_b a Y) (ϕ a).
+Proof.
+  hinduction Y ; try (intros; apply set_path2). 
+  - apply empty_isIn.
+  - intro b.
+    destruct (isIn_decidable a {|b|}).
+    * simpl in t.
+      strip_truncations.
+      rewrite t.
+      destruct (ϕ b).
+      ** rewrite (L_isIn_b_true _ _ idpath).
+         eauto with bool_lattice_hints.
+      ** rewrite empty_isIn ; rewrite (L_isIn_b_true _ _ idpath).
+         eauto with bool_lattice_hints.
+    * destruct (ϕ b).
+      ** rewrite L_isIn_b_false.
+         *** eauto with bool_lattice_hints.
+         *** intro. 
+             apply (n (tr X)).
+      ** rewrite empty_isIn.
+         rewrite L_isIn_b_false.
+         *** eauto with bool_lattice_hints.
+         *** intro.
+             apply (n (tr X)).
+  - intros.
+    Opaque isIn_b.
+    rewrite ?union_isIn.
+    rewrite X.
+    rewrite X0.
+    assert (forall b1 b2 b3,
+               (b1 && b2 || b3 && b2)%Bool = ((b1 || b3) && b2)%Bool).
+    { intros ; destruct b1, b2, b3 ; reflexivity. }
+    apply X1.
+Defined.
+End operations_isIn.
+
+Global Opaque isIn_b.
+(* Some suporting tactics *)
+Ltac simplify_isIn :=
+  repeat (rewrite union_isIn
+       || rewrite L_isIn_b_aa      
+       || rewrite intersection_isIn
+       || rewrite comprehension_isIn).
+  
+Ltac toBool := try (intro) ;
+    intros ; apply ext ; intros ; simplify_isIn ; eauto with bool_lattice_hints.
+
+Section SetLattice.
+
+  Context {A : Type}.
+  Context {A_deceq : DecidablePaths A}.
+  Context `{Univalence}.
+
+  Instance fset_union_com : Commutative (@U A).
+  Proof.
+    toBool.
+  Defined.
+
+  Instance fset_intersection_com : Commutative intersection.
+  Proof.
+    toBool.
+  Defined.
+
+  Instance fset_union_assoc : Associative (@U A).
+  Proof.
+    toBool.
+  Defined.
+
+  Instance fset_intersection_assoc : Associative intersection.
+  Proof.
+    toBool.
+  Defined.
+
+  Instance fset_union_idem : Idempotent (@U A).
+  Proof.
+    exact union_idem.
+  Defined.
+
+  Instance fset_intersection_idem : Idempotent intersection.
+  Proof.
+    toBool.
+  Defined.
+
+  Instance fset_union_nl : NeutralL (@U A) (@E A).
+  Proof.
+    toBool.
+  Defined.
+
+  Instance fset_union_nr : NeutralR (@U A) (@E A).
+  Proof.
+    toBool.
+  Defined.
+
+  Instance fset_absorption_intersection_union : Absorption (@U A) intersection.
+  Proof.
+    toBool.
+  Defined.
+
+  Instance fset_absorption_union_intersection : Absorption intersection (@U A).
+  Proof.
+    toBool.
+  Defined.
+  
+  Instance lattice_fset : Lattice intersection (@U A)  (@E A) :=
+    {
+      commutative_min := _ ;
+      commutative_max := _ ;
+      associative_min := _ ;
+      associative_max := _ ;
+      idempotent_min := _ ;
+      idempotent_max := _ ;
+      neutralL_min := _ ;
+      neutralR_min := _ ;
+      absorption_min_max := _ ;
+      absorption_max_min := _
+    }.
+
+End SetLattice.
+
+(* Comprehension properties *)
+Section comprehension_properties.
+
+  Opaque isIn_b.
+
+  Context {A : Type}.
+  Context {A_deceq : DecidablePaths A}.
+  Context `{Univalence}.
+
+  Lemma comprehension_or : forall ϕ ψ (x: FSet A),
+      comprehension (fun a => orb (ϕ a) (ψ a)) x
+      = U (comprehension ϕ x) (comprehension ψ x).
+  Proof.
+    toBool.
+  Defined.
+  
+  (** comprehension properties *)
+  Lemma comprehension_false Y : comprehension (fun (_ : A) => false) Y = E.
+  Proof.
+    toBool.
+  Defined.
+
+  Lemma comprehension_all : forall (X : FSet A),
+      comprehension (fun a => isIn_b a X) X = X.
+  Proof.
+    toBool.
+  Defined.
+  
+  Lemma comprehension_subset : forall ϕ (X : FSet A),
+    U (comprehension ϕ X) X = X.
+  Proof.
+    toBool.
+  Defined.
+  
+End comprehension_properties.
+
+(* With extensionality we can prove decidable equality *)
+Section dec_eq.
+  Context (A : Type) `{DecidablePaths A} `{Univalence}.
+
+  Instance decidable_prod {X Y : Type} `{Decidable X} `{Decidable Y} :
+    Decidable (X * Y).
+  Proof.
+    unfold Decidable in *.
+    destruct H1 as [x | nx] ; destruct H2 as [y | ny].
+    - left ; split ; assumption.
+    - right. intros [p1 p2]. contradiction.
+    - right. intros [p1 p2]. contradiction.
+    - right. intros [p1 p2]. contradiction.
+  Defined.
+    
+  Instance fsets_dec_eq : DecidablePaths (FSet A).
+  Proof.
+    intros X Y.
+    apply (decidable_equiv' ((subset Y X) * (subset X Y)) (eq_subset X Y)^-1).
+    apply _.
+  Defined.
+
+End dec_eq.