diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 3067ba33..46141271 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -35,7 +35,7 @@ jobs:
       - name: Install OCaml
         uses: avsm/setup-ocaml@v1
         with:
-          ocaml-version: 4.09.1
+          ocaml-version: 4.14.1
 
       # Checks-out your repository under $GITHUB_WORKSPACE, so your job can access it
       - name: Checkout repo
@@ -45,6 +45,6 @@ jobs:
       - name: Build
         run: |
           opam repo add coq-released https://coq.inria.fr/opam/released
-          opam install coq.8.16.0 coq-equations.1.3+8.16 coq-mathcomp-ssreflect.1.15.0 coq-mathcomp-analysis.0.5.3 coq-extructures.0.3.1 coq-deriving.0.1.0
+          opam install coq.8.18.0 coq-equations.1.3+8.18 coq-mathcomp-ssreflect.2.1.0 coq-mathcomp-analysis.1.0.0 coq-extructures.0.4.0 coq-deriving.0.2.0
           opam exec -- make -j4
 
diff --git a/_CoqProject b/_CoqProject
index 7acd4057..2da21a23 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -22,6 +22,7 @@ theories/Relational/Commutativity.v
 
 theories/Crypt/Prelude.v
 theories/Crypt/Axioms.v
+theories/Crypt/Casts.v
 theories/Crypt/choice_type.v
 
 # Categorical semantics
@@ -89,7 +90,7 @@ theories/Crypt/examples/KEMDEM.v
 theories/Crypt/examples/RandomOracle.v
 theories/Crypt/examples/SigmaProtocol.v
 theories/Crypt/examples/Schnorr.v
-theories/Crypt/examples/OVN.v
+# theories/Crypt/examples/OVN.v
 theories/Crypt/examples/Executor.v
 
 # Examples from https://github.com/Som1Lse/joy-of-ssprove
diff --git a/flake.lock b/flake.lock
new file mode 100644
index 00000000..49c856c9
--- /dev/null
+++ b/flake.lock
@@ -0,0 +1,60 @@
+{
+  "nodes": {
+    "flake-utils": {
+      "inputs": {
+        "systems": "systems"
+      },
+      "locked": {
+        "lastModified": 1705309234,
+        "narHash": "sha256-uNRRNRKmJyCRC/8y1RqBkqWBLM034y4qN7EprSdmgyA=",
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "rev": "1ef2e671c3b0c19053962c07dbda38332dcebf26",
+        "type": "github"
+      },
+      "original": {
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "type": "github"
+      }
+    },
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1707824078,
+        "narHash": "sha256-Au3wLi2d06bU7TDvahP2jIEeKwmjAxKHqi8l2uiBkGA=",
+        "owner": "nixos",
+        "repo": "nixpkgs",
+        "rev": "99d7b32e4cfdaf763d9335b4d9ecf4415cbdc405",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nixos",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "root": {
+      "inputs": {
+        "flake-utils": "flake-utils",
+        "nixpkgs": "nixpkgs"
+      }
+    },
+    "systems": {
+      "locked": {
+        "lastModified": 1681028828,
+        "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
+        "owner": "nix-systems",
+        "repo": "default",
+        "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nix-systems",
+        "repo": "default",
+        "type": "github"
+      }
+    }
+  },
+  "root": "root",
+  "version": 7
+}
diff --git a/flake.nix b/flake.nix
new file mode 100644
index 00000000..cf4bfc64
--- /dev/null
+++ b/flake.nix
@@ -0,0 +1,52 @@
+{
+  inputs = {
+    nixpkgs.url        = github:nixos/nixpkgs;
+    flake-utils.url    = github:numtide/flake-utils;
+  };
+  outputs = { self, nixpkgs, flake-utils }:
+    let
+      mkDrv = { stdenv, which, coqPackages, coq } :
+           let
+             extructures' = coqPackages.extructures.override { version = "0.4.0"; };
+           in
+            stdenv.mkDerivation {
+              pname = "ssprove";
+              version = "0.0.1";
+              src = ./.;
+              nativeBuildInputs = [ which coq.ocamlPackages.findlib ] ++
+                                  (with coqPackages; [
+                                    equations
+                                    mathcomp-analysis
+                                    mathcomp-ssreflect
+                                    deriving
+                                  ])
+                                  ++ [extructures'];
+              buildInputs = [ coq ];
+            };
+    in { inherit mkDrv; } //
+      flake-utils.lib.eachDefaultSystem (system:
+        let
+          pkgs = nixpkgs.legacyPackages.${system};
+        in
+         rec {
+            devShell =
+              let
+                args = {
+                  inherit (pkgs) stdenv which;
+                  coq = pkgs.coq_8_18;
+                  coqPackages = pkgs.coqPackages_8_18.overrideScope
+                    (self: super: {
+                      mathcomp = super.mathcomp.override { version = "2.1.0"; };
+                      mathcomp-analysis = super.mathcomp-analysis.override { version = "1.0.0"; };
+                    });
+                };
+                ssprove' = mkDrv args;
+              in
+                pkgs.mkShell {
+                  packages =
+                    (with pkgs; [ coq gnumake ])
+                    ++
+                    (with ssprove';  nativeBuildInputs);
+                };
+         });
+}
diff --git a/ssprove.opam b/ssprove.opam
index 2a8828f4..89a745ef 100644
--- a/ssprove.opam
+++ b/ssprove.opam
@@ -8,12 +8,12 @@ homepage: "https://github.com/SSProve/ssprove"
 bug-reports: "https://github.com/SSProve/ssprove/issues"
 license: "MIT"
 depends: [
-  "coq" {(>= "8.16" & < "8.18~")}
-  "coq-equations" {>= "1.3"}
-  "coq-mathcomp-ssreflect" {(>= "1.15.0" & < "1.17~")}
-  "coq-mathcomp-analysis" {>= "0.5.3" & <= "0.6.1"}
-  "coq-extructures" {(>= "0.3.1" & < "dev")}
-  "coq-deriving" {(>= "0.1" & < "dev")}
+  "coq" {(>= "8.18~")}
+  "coq-equations" {(>= "1.3+8.18")}
+  "coq-mathcomp-ssreflect" {(>= "2.1.0")}
+  "coq-mathcomp-analysis" {>= "1.0.0"}
+  "coq-extructures" {(>= "0.4.0" & < "dev")}
+  "coq-deriving" {(>= "0.2.0" & < "dev")}
 ]
 build: [
   [make "-j%{jobs}%"]
diff --git a/theories/Crypt/Casts.v b/theories/Crypt/Casts.v
new file mode 100644
index 00000000..4efd278c
--- /dev/null
+++ b/theories/Crypt/Casts.v
@@ -0,0 +1,37 @@
+Set Warnings "-ambiguous-paths,-notation-overridden,-notation-incompatible-format".
+From mathcomp Require Import ssreflect ssrbool ssrnat choice fintype.
+Set Warnings "ambiguous-paths,notation-overridden,notation-incompatible-format".
+
+From extructures Require Import ord fmap.
+From Crypt Require Import Prelude.
+
+From HB Require Import structures.
+
+
+(**
+  Note for any of these types it would also be okay to write the cast, e.g., [(nat:choiceType)%type],
+  directly in the term.
+  This (backward-compatibility) file just made porting to mathcomp 2.1.0 easier.
+  Just delete as soon as all references to the below casts are gone from the code base.
+ *)
+
+Definition unit_choiceType : choiceType := Datatypes.unit.
+Definition nat_choiceType : choiceType := nat.
+Definition bool_choiceType : choiceType := bool.
+Definition prod_choiceType (A B: choiceType) : choiceType := prod A B.
+Definition fmap_choiceType (A: ordType) (B: choiceType) : choiceType := {fmap A -> B}.
+Definition option_choiceType (A: choiceType) : choiceType := option A.
+Definition fin_choiceType (p: positive) : choiceType := ordinal p.(pos).
+Definition sum_choiceType (A B: choiceType) : choiceType := (A + B)%type.
+
+Definition unit_ordType: ordType := Datatypes.unit.
+Definition nat_ordType: ordType := nat.
+Definition bool_ordType: ordType := bool.
+Definition prod_ordType (A B: ordType) : ordType := prod A B.
+Definition fmap_ordType (A B: ordType) : ordType := {fmap A -> B}.
+Definition option_ordType (A: ordType) : ordType := option A.
+Definition fin_ordType (p: positive) : ordType := ordinal p.(pos).
+Definition sum_ordType (A B: ordType) : ordType := (A + B)%type.
+
+
+Definition prod_finType (A B: finType) : finType := prod A B.
diff --git a/theories/Crypt/Prelude.v b/theories/Crypt/Prelude.v
index df763081..7898b94b 100644
--- a/theories/Crypt/Prelude.v
+++ b/theories/Crypt/Prelude.v
@@ -5,6 +5,7 @@ From Coq Require Import Utf8 Lia.
 Set Warnings "-notation-overridden".
 From mathcomp Require Import ssreflect eqtype ssrbool ssrnat.
 Set Warnings "notation-overridden".
+From HB Require Import structures.
 From extructures Require Import ord fset.
 From Equations Require Import Equations.
 From Mon Require SPropBase.
@@ -180,9 +181,7 @@ Proof.
     intro h. apply e. inversion h. reflexivity.
 Qed.
 
-Canonical positive_eqMixin := EqMixin positive_eqP.
-  Canonical positive_eqType :=
-    Eval hnf in EqType positive positive_eqMixin.
+HB.instance Definition _ := hasDecEq.Build _ positive_eqP.
 
 (** Lt class, for finite types  *)
 
@@ -314,4 +313,4 @@ Definition testSome {A} (P : A → bool) (o : option A) : bool :=
   match o with
   | Some a => P a
   | None => false
-  end.
\ No newline at end of file
+  end.
diff --git a/theories/Crypt/choice_type.v b/theories/Crypt/choice_type.v
index 0a12499b..ed58c95c 100644
--- a/theories/Crypt/choice_type.v
+++ b/theories/Crypt/choice_type.v
@@ -9,11 +9,15 @@
 From Coq Require Import Utf8 Lia.
 From Relational Require Import OrderEnrichedCategory
   OrderEnrichedRelativeMonadExamples GenericRulesSimple.
+
 Set Warnings "-ambiguous-paths,-notation-overridden,-notation-incompatible-format".
 From mathcomp Require Import ssrnat ssreflect ssrfun ssrbool ssrnum eqtype
   choice reals distr realsum seq all_algebra fintype.
 Set Warnings "ambiguous-paths,notation-overridden,notation-incompatible-format".
-From Crypt Require Import Prelude Axioms.
+From HB Require Import structures.
+
+From Crypt Require Import Prelude Axioms Casts.
+From deriving Require Import deriving.
 From extructures Require Import ord fset fmap.
 From Mon Require Import SPropBase.
 Require Equations.Prop.DepElim.
@@ -44,13 +48,6 @@ Inductive choice_type :=
 
 Derive NoConfusion NoConfusionHom for choice_type.
 
-(* Definition void_leq (x y : void) := true. *)
-
-(* Lemma void_leqP : Ord.axioms void_leq. *)
-(* Proof. split; by do ![case]. Qed. *)
-
-(* Definition void_ordMixin := OrdMixin void_leqP. *)
-(* Canonical void_ordType := Eval hnf in OrdType void void_ordMixin. *)
 
 Fixpoint chElement_ordType (U : choice_type) : ordType :=
   match U with
@@ -60,7 +57,7 @@ Fixpoint chElement_ordType (U : choice_type) : ordType :=
   | chProd U1 U2 => prod_ordType (chElement_ordType U1) (chElement_ordType U2)
   | chMap U1 U2 => fmap_ordType (chElement_ordType U1) (chElement_ordType U2)
   | chOption U => option_ordType (chElement_ordType U)
-  | chFin n => [ordType of ordinal n.(pos) ]
+  | chFin n => fin_ordType n
   end.
 
 Fixpoint chElement (U : choice_type) : choiceType :=
@@ -71,7 +68,7 @@ Fixpoint chElement (U : choice_type) : choiceType :=
   | chProd U1 U2 => prod_choiceType (chElement U1) (chElement U2)
   | chMap U1 U2 => fmap_choiceType (chElement_ordType U1) (chElement U2)
   | chOption U => option_choiceType (chElement U)
-  | chFin n => [choiceType of ordinal n.(pos) ]
+  | chFin n => fin_choiceType n
   end.
 
 Coercion chElement : choice_type >-> choiceType.
@@ -149,9 +146,21 @@ Section choice_typeTypes.
     - move: e => /choice_type_eqP []. reflexivity.
   Qed.
 
-  Canonical choice_type_eqMixin := EqMixin choice_type_eqP.
-  Canonical choice_type_eqType :=
-    Eval hnf in EqType choice_type choice_type_eqMixin.
+  Definition choice_type_indDef := [indDef for choice_type_rect].
+  Canonical choice_type_indType := IndType choice_type choice_type_indDef.
+  (* The unfolding became a problem in [pkg_composition]. So I follow the advice on
+     https://github.com/arthuraa/deriving
+   *)
+
+  (*
+    This
+    [Definition choice_type_hasDecEq := [derive hasDecEq for choice_type].]
+    did work well up until [pkg_composition].
+    The unfolding there was too much.
+    The [nored] version then did not provide enough reduction.
+   *)
+  Definition choice_type_hasDecEq := hasDecEq.Build choice_type choice_type_eqP.
+  HB.instance Definition _ := choice_type_hasDecEq.
 
   Fixpoint choice_type_lt (t1 t2 : choice_type) :=
   match t1, t2 with
@@ -169,7 +178,7 @@ Section choice_typeTypes.
   | chProd _ _, chNat => false
   | chProd u1 u2, chProd w1 w2 =>
     (choice_type_lt u1 w1) ||
-    (choice_type_eq u1 w1 && choice_type_lt u2 w2)
+    (eq_op u1 w1 && choice_type_lt u2 w2)
   | chProd _ _, _ => true
   | chMap _ _, chUnit => false
   | chMap _ _, chBool => false
@@ -177,7 +186,7 @@ Section choice_typeTypes.
   | chMap _ _, chProd _ _ => false
   | chMap u1 u2, chMap w1 w2 =>
     (choice_type_lt u1 w1) ||
-    (choice_type_eq u1 w1 && choice_type_lt u2 w2)
+    (eq_op u1 w1 && choice_type_lt u2 w2)
   | chMap _ _, _ => true
   | chOption _, chUnit => false
   | chOption _, chBool => false
@@ -196,7 +205,7 @@ Section choice_typeTypes.
   end.
 
   Definition choice_type_leq (t1 t2 : choice_type) :=
-    choice_type_eq t1 t2 || choice_type_lt t1 t2.
+    eq_op t1 t2 || choice_type_lt t1 t2.
 
   Lemma choice_type_lt_transitive : transitive (T:=choice_type) choice_type_lt.
   Proof.
@@ -270,20 +279,18 @@ Section choice_typeTypes.
 
   Lemma choice_type_lt_total_holds :
     ∀ x y,
-      ~~ (choice_type_test x y) ==> (choice_type_lt x y || choice_type_lt y x).
+      ~~ (eq_op x y) ==> (choice_type_lt x y || choice_type_lt y x).
   Proof.
-    intros x y.
-    induction x as [ | | | x1 ih1 x2 ih2| x1 ih1 x2 ih2| x ih| x]
-    in y |- *.
+    intros x.
+    induction x as [ | | | x1 ih1 x2 ih2| x1 ih1 x2 ih2| x ih| x].
     all: try solve [ destruct y ; auto with solve_subterm; reflexivity ].
     - destruct y. all: try (intuition; reflexivity).
-      cbn.
       specialize (ih1 y1). specialize (ih2 y2).
       apply/implyP.
-      move /nandP => H.
-      apply/orP.
-      destruct (choice_type_test x1 y1) eqn:Heq.
-      + destruct H. 1: discriminate.
+      move/nandP; rewrite -/choice_type_test -/eq_op.
+      move => H; apply/orP.
+      destruct (eq_op x1 y1) eqn:Heq.
+      + setoid_rewrite -> Heq in H. move/nandP: H; rewrite Bool.andb_true_l => H.
         move: ih2. move /implyP => ih2.
         specialize (ih2 H).
         move: ih2. move /orP => ih2.
@@ -293,7 +300,7 @@ Section choice_typeTypes.
         * right. apply/orP. right. apply/andP. intuition.
           move: Heq. move /eqP => Heq. rewrite Heq. apply/eqP. reflexivity.
       + destruct H.
-        * move: ih1. move /implyP => ih1.
+        * move: ih1. rewrite -Heq; move /implyP => ih1.
           specialize (ih1 H).
           move: ih1. move /orP => ih1.
           destruct ih1.
@@ -317,8 +324,8 @@ Section choice_typeTypes.
       apply/implyP.
       move /nandP => H.
       apply/orP.
-      destruct (choice_type_test x1 y1) eqn:Heq.
-      + destruct H. 1: discriminate.
+      destruct (eq_op x1 y1) eqn:Heq.
+      + setoid_rewrite -> Heq in H; move: H => /nandP H; simpl in H.
         move: ih2. move /implyP => ih2.
         specialize (ih2 H).
         move: ih2. move /orP => ih2.
@@ -328,7 +335,7 @@ Section choice_typeTypes.
         * right. apply/orP. right. apply/andP. intuition.
           move: Heq. move /eqP => Heq. rewrite Heq. apply/eqP. reflexivity.
       + destruct H.
-        * move: ih1. move /implyP => ih1.
+        * move: ih1. rewrite -Heq; move /implyP => ih1.
           specialize (ih1 H).
           move: ih1. move /orP => ih1.
           destruct ih1.
@@ -347,10 +354,9 @@ Section choice_typeTypes.
               +++ left. apply/orP. left. assumption.
               +++ right. apply/orP. left. assumption.
     - destruct y. all: try (intuition; reflexivity).
-      unfold choice_type_lt.
-      unfold choice_type_test.
+      rewrite /choice_type_lt.
       rewrite -neq_ltn.
-      apply /implyP. auto.
+      by [apply/implyP].
   Qed.
 
   Lemma choice_type_lt_asymmetric :
@@ -370,7 +376,7 @@ Section choice_typeTypes.
 
   Lemma choice_type_lt_total_not_holds :
     ∀ x y,
-      ~~ (choice_type_test x y) ==> (~~ (choice_type_lt x y && choice_type_lt y x)).
+      ~~ (eq_op x y) ==> (~~ (choice_type_lt x y && choice_type_lt y x)).
   Proof.
     intros x y. apply /implyP. intros Hneq.
     pose (choice_type_lt_total_holds x y) as Htot.
@@ -384,67 +390,75 @@ Section choice_typeTypes.
 
   Lemma choice_type_lt_tot :
     ∀ x y,
-      (choice_type_lt x y || choice_type_lt y x || choice_type_eq x y).
+      (choice_type_lt x y || choice_type_lt y x || eq_op x y).
   Proof.
     intros x y.
-    destruct (choice_type_eq x y) eqn:H.
+    destruct (eq_op x y) eqn:H.
     - apply/orP.
       by right.
     - apply/orP.
       left.
-      unfold choice_type_eq in H.
       pose (choice_type_lt_total_holds x y).
       move: i. move /implyP => i.
       apply i. apply/negP.
       intuition. move: H0. rewrite H. intuition.
   Qed.
 
-  Lemma choice_type_leqP : Ord.axioms choice_type_leq.
+  Lemma choice_type_leqxx : reflexive choice_type_leq.
   Proof.
-    split => //.
-    - intro x. unfold choice_type_leq.
-      apply/orP. left. apply /eqP. reflexivity.
-    - intros v u w h1 h2.
-      move: h1 h2. unfold choice_type_leq.
-      move /orP => h1. move /orP => h2.
-      destruct h1.
-      + move: H. move /eqP => H. destruct H.
-        apply/orP. assumption.
-      + destruct h2.
-        * move: H0. move /eqP => H0. destruct H0.
-          apply/orP. right. assumption.
-        * apply/orP. right. exact (choice_type_lt_transitive _ _ _ H H0).
-    - unfold antisymmetric.
-      move => x y. unfold choice_type_leq. move/andP => [h1 h2].
-      move: h1 h2. unfold choice_type_leq.
-      move /orP => h1. move /orP => h2.
-      destruct h1.
-      1:{ move: H. move /eqP. intuition auto. }
-      destruct h2.
-      1:{ move: H0. move /eqP. intuition auto. }
-      destruct (~~ (choice_type_test x y)) eqn:Heq.
-      + move: Heq. move /idP => Heq.
-        pose (choice_type_lt_total_not_holds x y) as Hp.
-        move: Hp. move /implyP => Hp. specialize (Hp Heq).
-        move: Hp. move /nandP => Hp.
-        destruct Hp.
-        * move: H. move /eqP /eqP => H. rewrite H in H1. simpl in H1.
-          discriminate.
-        * move: H0. move /eqP /eqP => H0. rewrite H0 in H1. simpl in H1.
-          discriminate.
-      + move: Heq. move /eqP. auto.
-    - unfold total.
-      intros x y. unfold choice_type_leq.
-      pose (choice_type_lt_tot x y).
-      move: i. move /orP => H.
-      destruct H.
-      + move: H. move /orP => H.
-        destruct H.
-        * apply/orP. left. apply/orP. right. assumption.
-        * apply/orP. right. apply/orP. right. assumption.
-      + apply/orP. left. apply/orP. left. assumption.
+    move => x; rewrite /choice_type_leq.
+    by [apply/orP; left; apply/eqP].
   Qed.
 
+  Lemma choice_type_leq_trans : transitive choice_type_leq.
+  Proof.
+    move => v u w; rewrite /choice_type_leq.
+    move/orP => h1; move/orP => h2.
+    case: h1.
+    + by [move/eqP => ih1; rewrite ih1; apply/orP].
+    + case: h2.
+      * move /eqP => H0; rewrite H0 => lt_u_w.
+        by [apply/orP; right].
+      * move => lt_v_w lt_u_v.
+        apply/orP; right.
+        exact: (choice_type_lt_transitive _ _ _ lt_u_v lt_v_w).
+  Qed.
+
+  Lemma choice_type_leq_asym : antisymmetric choice_type_leq.
+  Proof.
+    move => x y; rewrite /choice_type_leq; move/andP.
+    rewrite /choice_type_leq.
+    case.
+    move/orP => h1; move/orP => h2.
+    case: h1.
+    - by [move/eqP].
+    - case: h2.
+      + by [move/eqP].
+      + case Heq: (~~ (eq_op x y)).
+        * move: Heq. move /idP => Heq.
+          pose (choice_type_lt_total_not_holds x y) as Hp.
+          move: Hp. move /implyP => Hp. specialize (Hp Heq).
+          move: Hp. move /nandP => Hp.
+          case: Hp.
+          ** move/eqP => nlt_x_y lt_y_x; move/eqP/eqP => lt_x_y.
+             by [move: nlt_x_y; rewrite lt_x_y /=; move/eqP].
+          ** move/eqP => nlt_y_x lt_y_x; move/eqP/eqP => lt_x_y.
+             by [move: nlt_y_x; rewrite lt_y_x /=; move/eqP].
+      * by [move: Heq; move /eqP].
+  Qed.
+
+  Lemma choice_type_leq_total : total choice_type_leq.
+  Proof.
+    move => x y; rewrite /choice_type_leq.
+    pose (choice_type_lt_tot x y).
+    move: i => /orP i.
+    case: i.
+    + move/orP => i.
+      case: i => [lt_x_y|lt_y_x]; apply/orP.
+      * by [left; apply/orP; right].
+      * by [right; apply/orP; right].
+    + by [move => i; apply/orP; left; apply/orP; left].
+  Qed.
 
   Fixpoint encode (t : choice_type) : GenTree.tree nat :=
   match t with
@@ -497,12 +511,14 @@ Section choice_typeTypes.
         rewrite -subnE subn0. repeat f_equal. apply eq_irrelevance.
   Defined.
 
-  Definition choice_type_choiceMixin := PcanChoiceMixin codeK.
-  Canonical choice_type_choiceType :=
-    ChoiceType choice_type choice_type_choiceMixin.
+  HB.instance Definition _ := Choice.copy choice_type (pcan_type codeK).
 
-  Definition choice_type_ordMixin := OrdMixin choice_type_leqP.
-  Canonical choice_type_ordType :=
-    Eval hnf in OrdType choice_type choice_type_ordMixin.
+  HB.instance Definition _ :=
+    hasOrd.Build
+      choice_type
+      choice_type_leqxx
+      choice_type_leq_trans
+      choice_type_leq_asym
+      choice_type_leq_total.
 
 End choice_typeTypes.
diff --git a/theories/Crypt/examples/DDH.v b/theories/Crypt/examples/DDH.v
index 09e54465..2585e24f 100644
--- a/theories/Crypt/examples/DDH.v
+++ b/theories/Crypt/examples/DDH.v
@@ -56,7 +56,7 @@ Module DDH (DDHP : DDHParams) (GP : GroupParam).
 
   #[local] Existing Instance Space_pos.
 
-  Definition GroupSpace : finType := FinGroup.arg_finType gT.
+  Definition GroupSpace : finType := gT.
   #[local] Instance GroupSpace_pos : Positive #|GroupSpace|.
   Proof.
     apply /card_gt0P; by exists g.
diff --git a/theories/Crypt/examples/ElGamal.v b/theories/Crypt/examples/ElGamal.v
index a24f3d90..40a9829b 100644
--- a/theories/Crypt/examples/ElGamal.v
+++ b/theories/Crypt/examples/ElGamal.v
@@ -79,12 +79,11 @@ Qed.
 
 Module MyParam <: AsymmetricSchemeParams.
 
-  Definition SecurityParameter : choiceType := nat_choiceType.
-  Definition Plain  : finType := FinGroup.arg_finType gT.
-  Definition Cipher : finType :=
-    prod_finType (FinGroup.arg_finType gT) (FinGroup.arg_finType gT).
-  Definition PubKey : finType := FinGroup.arg_finType gT.
-  Definition SecKey : finType := [finType of 'Z_q].
+  Definition SecurityParameter : choiceType := nat.
+  Definition Plain  : finType := gT.
+  Definition Cipher : finType := prod (gT:finType) (gT:finType).
+  Definition PubKey : finType := gT.
+  Definition SecKey : finType := Finite.clone _ 'Z_q.
 
   Definition plain0 := g.
   Definition cipher0 := (g, g).
@@ -479,7 +478,7 @@ End ElGamal.
 
 Module EGP_Z3 <: ElGamalParam.
 
-  Definition gT : finGroupType := Zp_finGroupType 2.
+  Definition gT : finGroupType := 'Z_2.
   Definition ζ : {set gT} := [set : gT].
   Definition g :  gT := Zp1.
 
diff --git a/theories/Crypt/examples/KEMDEM.v b/theories/Crypt/examples/KEMDEM.v
index 142a1e72..9df1e822 100644
--- a/theories/Crypt/examples/KEMDEM.v
+++ b/theories/Crypt/examples/KEMDEM.v
@@ -604,7 +604,7 @@ Section KEMDEM.
     as ineq.
     eapply le_trans. 1: exact ineq.
     clear ineq.
-    eapply ler_add.
+    eapply lerD.
     (* Idealising the core keying package *)
     - replace (par CK₀ CD₀) with ((par (ID EK) CD₀) ∘ (par CK₀ (ID IGET))).
       2:{
@@ -696,7 +696,7 @@ Section KEMDEM.
     as ineq.
     eapply le_trans. 1: exact ineq.
     clear ineq.
-    eapply ler_add.
+    eapply lerD.
     - eapply single_key_a. all: eauto.
     (* De-idealising the core keying package *)
     - replace (par CK₀ CD₁) with ((par (ID EK) CD₁) ∘ (par CK₀ (ID IGET))).
@@ -1065,4 +1065,4 @@ Section KEMDEM.
       all: fdisjoint_auto.
   Qed.
 
-End KEMDEM.
\ No newline at end of file
+End KEMDEM.
diff --git a/theories/Crypt/examples/OTP.v b/theories/Crypt/examples/OTP.v
index 78e3315e..8cf2f8c5 100644
--- a/theories/Crypt/examples/OTP.v
+++ b/theories/Crypt/examples/OTP.v
@@ -63,9 +63,9 @@ Section OTP_example.
 
   Definition N_pos : Positive N := _.
 
-  Definition Words : finType := [finType of 'Z_N].
+  Definition Words : finType := Finite.clone _ 'Z_N.
 
-  Definition Key : finType := [finType of 'Z_N].
+  Definition Key : finType := Finite.clone _ 'Z_N.
 
   Definition w0 : Words := 0.
 
diff --git a/theories/Crypt/examples/OVN.v b/theories/Crypt/examples/OVN.v
index 6864d6f9..0f687225 100644
--- a/theories/Crypt/examples/OVN.v
+++ b/theories/Crypt/examples/OVN.v
@@ -9,7 +9,7 @@ Set Warnings "notation-overridden,ambiguous-paths".
 
 From Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings
   UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb UniformStateProb
-  pkg_composition Package Prelude SigmaProtocol Schnorr DDH.
+  pkg_composition Package Prelude SigmaProtocol Schnorr DDH Canonicals.
 
 From Coq Require Import Utf8 Lia.
 From extructures Require Import ord fset fmap.
@@ -100,9 +100,9 @@ Proof.
   reflexivity.
 Qed.
 
-Definition Pid : finType := [finType of 'I_n].
-Definition Secret : finType := Zp_finComRingType (Zp_trunc #[g]).
-Definition Public : finType := FinGroup.arg_finType gT.
+Definition Pid : finType := Finite.clone _ 'I_n.
+Definition Secret : finComRingType := 'Z_(Zp_trunc #[g]).
+Definition Public : finType := gT.
 Definition s0 : Secret := 0.
 
 Definition Pid_pos : Positive #|Pid|.
@@ -263,7 +263,22 @@ Module OVN (π2 : CDSParams) (Alg2 : SigmaProtocolAlgorithms π2).
     | _ => 1
     end.
 
+  From HB Require Import structures.
+  (*HB.about Monoid.ComLaw.
+  HB.howto Monoid.ComLaw.type.
+  HB.about Monoid.isComLaw.Build.
+  HB.about Monoid.ComLaw.
+  Check group_prodC.
+  Locate group_prodC.
+  Print mulg.
+  Locate "*".
+  Print commutative.
+  HB.about Monoid.isComLaw.
+   *)
+  (*
+  HB.instance Definition _ := Monoid.isComLaw.Build gT [1 gT] mulg group_prodA group_prodC group_1prod.
   Canonical finGroup_com_law := Monoid.ComLaw group_prodC.
+   *)
 
   Definition compute_key
              (m : chMap pid (chProd public choiceTranscript1))
@@ -304,7 +319,6 @@ Module OVN (π2 : CDSParams) (Alg2 : SigmaProtocolAlgorithms π2).
     rewrite !big_fsetU1.
     2-3: subst X; apply not_in_domm.
     rewrite setm_rem.
-
     have set_rem_eq : forall P x,
       \big[finGroup_com_law/1]_(k <- X :\ j | P k)
         get_value (setm keys j x) k =
@@ -327,8 +341,8 @@ Module OVN (π2 : CDSParams) (Alg2 : SigmaProtocolAlgorithms π2).
         rewrite eq_refl in contra.
         discriminate.
       - reflexivity.
-    }
 
+    }
     case (j < i)%ord eqn:e.
     - rewrite !e.
       rewrite -2!mulgA.
@@ -2194,3 +2208,4 @@ Module OVN (π2 : CDSParams) (Alg2 : SigmaProtocolAlgorithms π2).
 
 End OVN.
 End OVN.
+
diff --git a/theories/Crypt/examples/PRFPRG.v b/theories/Crypt/examples/PRFPRG.v
index 750d48d0..9fe35fcb 100644
--- a/theories/Crypt/examples/PRFPRG.v
+++ b/theories/Crypt/examples/PRFPRG.v
@@ -394,7 +394,7 @@ Proof.
   move: {ineq H1 H2 H3} (H1, H2, H3) => H.
   rewrite GEN_GEN_HYB_equiv ?fdisjointUr ?H // GRing.addr0.
   rewrite GEN_GEN_HYB_EVAL_equiv ?fdisjointUr ?H // GRing.addr0.
-  rewrite big_ord_recr ler_add //.
+  rewrite big_ord_recr lerD //.
   by rewrite /prf_epsilon Advantage_E Advantage_link Advantage_sym.
 Qed.
 
diff --git a/theories/Crypt/examples/Schnorr.v b/theories/Crypt/examples/Schnorr.v
index 85c54b56..a1633071 100644
--- a/theories/Crypt/examples/Schnorr.v
+++ b/theories/Crypt/examples/Schnorr.v
@@ -12,7 +12,7 @@ From Mon Require Import SPropBase.
 From Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings
   UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb UniformStateProb
   pkg_core_definition choice_type pkg_composition pkg_rhl Package Prelude
-  SigmaProtocol.
+  SigmaProtocol Casts.
 
 From Coq Require Import Utf8.
 From extructures Require Import ord fset fmap.
@@ -54,13 +54,13 @@ Definition q : nat := #[g].
 
 Module MyParam <: SigmaProtocolParams.
 
-  Definition Witness : finType := [finType of 'Z_q].
-  Definition Statement : finType := FinGroup.arg_finType gT.
-  Definition Message : finType := FinGroup.arg_finType gT.
-  Definition Challenge : finType := [finType of 'Z_q].
-  Definition Response : finType :=  [finType of 'Z_q].
-  Definition Transcript :=
-    prod_finType (prod_finType Message Challenge) Response.
+  Definition Witness : finType := Finite.clone _ 'Z_q.
+  Definition Statement : finType := gT.
+  Definition Message : finType := gT.
+  Definition Challenge : finType := Finite.clone _ 'Z_q.
+  Definition Response : finType :=  Finite.clone _ 'Z_q.
+  Definition Transcript : finType :=
+    prod (prod Message Challenge) Response.
 
   Definition w0 : Witness := 0.
   Definition e0 : Challenge := 0.
@@ -83,7 +83,7 @@ Module MyParam <: SigmaProtocolParams.
   Definition Message_pos : Positive #|Message| := _.
   Definition Challenge_pos : Positive #|Challenge| := _.
   Definition Response_pos : Positive #|Response| := _.
-  Definition Bool_pos : Positive #|bool_choiceType|.
+  Definition Bool_pos : Positive #|(bool:choiceType)|.
   Proof.
     rewrite card_bool. done.
   Defined.
@@ -286,7 +286,7 @@ Proof.
 Qed.
 
 Lemma neq_pos :
-  ∀ (q : nat) (a b : Zp_finZmodType q),
+  ∀ (q : nat) (a b : ('Z_q:finZmodType)),
     a != b →
     a - b != 0.
 Proof.
@@ -371,8 +371,9 @@ Proof.
     (modn
        (addn (@nat_of_ord (S (S (Zp_trunc q))) (@otf Challenge s1))
              (@nat_of_ord (S (S (Zp_trunc q)))
-                          (@GRing.opp (FinRing.Zmodule.zmodType (Zp_finZmodType (S (Zp_trunc q))))
-                                      (@otf Challenge s2)))) q) =
+                (GRing.opp
+                   (@otf Challenge s2))))
+       q) =
     (@nat_of_ord (S (S (Zp_trunc q)))
                    (@Zp_add (S (Zp_trunc q)) (@otf Challenge s1) (@Zp_opp (S (Zp_trunc q)) (@otf Challenge s2)))).
   { simpl.
@@ -393,19 +394,19 @@ Proof.
   have -> :
     (modn
        (muln (@nat_of_ord (S (S (Zp_trunc q)))
-                          (@GRing.inv (FinRing.UnitRing.unitRingType (Zp_finUnitRingType (Zp_trunc q)))
-                                      (@GRing.add (FinRing.Zmodule.zmodType (Zp_finZmodType (S (Zp_trunc q))))
-                                                  (@otf Challenge s1)
-                                                  (@GRing.opp (FinRing.Zmodule.zmodType (Zp_finZmodType (S (Zp_trunc q))))
-                                                              (@otf Challenge s2)))))
-             (@nat_of_ord (S (S (Zp_trunc q)))
-                          (@Zp_add (S (Zp_trunc q)) (@otf Challenge s1) (@Zp_opp (S (Zp_trunc q)) (@otf Challenge s2))))) q) =
+                (GRing.inv
+                   (GRing.add
+                      (@otf Challenge s1)
+                      (GRing.opp
+                         (@otf Challenge s2)))))
+          (@nat_of_ord (S (S (Zp_trunc q)))
+             (@Zp_add (S (Zp_trunc q)) (@otf Challenge s1) (@Zp_opp (S (Zp_trunc q)) (@otf Challenge s2))))) q) =
     (Zp_mul
-       (@GRing.inv (FinRing.UnitRing.unitRingType (Zp_finUnitRingType (Zp_trunc q)))
-                   (@GRing.add (FinRing.Zmodule.zmodType (Zp_finZmodType (S (Zp_trunc q))))
-                               (@otf Challenge s1)
-                               (@GRing.opp (FinRing.Zmodule.zmodType (Zp_finZmodType (S (Zp_trunc q))))
-                                           (@otf Challenge s2))))
+       (GRing.inv
+          (GRing.add
+             (@otf Challenge s1)
+             (GRing.opp
+                (@otf Challenge s2))))
        (@Zp_add (S (Zp_trunc q)) (@otf Challenge s1) (@Zp_opp (S (Zp_trunc q)) (@otf Challenge s2)))).
   { simpl.
     rewrite modnDmr.
@@ -665,7 +666,7 @@ End Schnorr.
 
 Module GP_Z3 <: GroupParam.
 
-  Definition gT : finGroupType := Zp_finGroupType 2.
+  Definition gT : finGroupType := 'Z_2.
   Definition ζ : {set gT} := [set : gT].
   Definition g :  gT := Zp1.
 
diff --git a/theories/Crypt/examples/ShamirSecretSharing.v b/theories/Crypt/examples/ShamirSecretSharing.v
index 7d881cda..5fff74f9 100644
--- a/theories/Crypt/examples/ShamirSecretSharing.v
+++ b/theories/Crypt/examples/ShamirSecretSharing.v
@@ -481,7 +481,7 @@ Proof.
   rewrite /nilp size_poly_eq0 in Heq.
   move /eqP in Heq.
   rewrite Heq polyseqC.
-  by destruct (a != 0).
+  by case: (a != 0).
 Qed.
 
 Lemma size_tail_poly {R: ringType} (q: {poly R}):
@@ -927,7 +927,7 @@ Proof.
   }
   rewrite addn0 IHt ?cons_head_tail_poly //.
   rewrite size_tail_poly.
-  by destruct (size q).
+  destruct (size q) eqn:P; by rewrite P.
 Qed.
 
 (**
diff --git a/theories/Crypt/examples/SigmaProtocol.v b/theories/Crypt/examples/SigmaProtocol.v
index f0a117a6..bb5ae4b1 100644
--- a/theories/Crypt/examples/SigmaProtocol.v
+++ b/theories/Crypt/examples/SigmaProtocol.v
@@ -10,7 +10,7 @@ Set Warnings "notation-overridden,ambiguous-paths".
 From Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings
   UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb UniformStateProb
   pkg_core_definition choice_type pkg_composition pkg_rhl
-  Package Prelude RandomOracle.
+  Package Prelude RandomOracle Casts.
 
 From Coq Require Import Utf8.
 From extructures Require Import ord fset fmap.
@@ -520,7 +520,7 @@ Module SigmaProtocol (π : SigmaProtocolParams)
       as ineq.
       eapply le_trans. 1: exact ineq.
       clear ineq.
-      repeat eapply ler_add.
+      repeat eapply lerD.
       - apply eq_ler.
         eapply eq_rel_perf_ind with (inv := inv).
         5: apply VA.
diff --git a/theories/Crypt/examples/concrete_groups.v b/theories/Crypt/examples/concrete_groups.v
index a7c2874e..0c05f838 100644
--- a/theories/Crypt/examples/concrete_groups.v
+++ b/theories/Crypt/examples/concrete_groups.v
@@ -6,7 +6,7 @@ Set Warnings "-notation-overridden,-ambiguous-paths,-notation-incompatible-forma
 From mathcomp Require Import all_ssreflect fingroup.fingroup fintype
      eqtype choice seq.
 Set Warnings "notation-overridden,ambiguous-paths,notation-incompatible-format".
-
+From HB Require Import structures.
 From deriving Require Import deriving.
 
 Set Bullet Behavior "Strict Subproofs".
@@ -42,29 +42,27 @@ Module Z2_manual.
     ltac:(move => [|] [|];
             try solve [ right ; discriminate ];
             try solve [ left ; reflexivity ]).
-  Definition Z2_eqMixin := EqMixin Z2_eqP.
-  Canonical Z2_eqType : eqType :=
-    Eval hnf in EqType Z2 Z2_eqMixin.
+  Definition Z2_hasDecEq := hasDecEq.Build Z2 Z2_eqP.
+  HB.instance Definition _ := Z2_hasDecEq.
 
   Definition Z2_pickle x : nat := match x with z => 0 | o => 1 end.
   Definition Z2_unpickle (x : nat) := match x with 0 => Some z | 1 => Some o | _ => None end.
   Lemma Z2_p_u_cancel : @pcancel nat Z2 Z2_pickle Z2_unpickle.
   Proof. move => [|] //. Qed.
 
-  Definition Z2_choiceMixin := PcanChoiceMixin Z2_p_u_cancel.
-  Canonical Z2_choiceType := ChoiceType Z2 Z2_choiceMixin.
+  HB.instance Definition _ := Choice.copy Z2 (pcan_type Z2_p_u_cancel).
 
-  Definition Z2_countMixin := @choice.Countable.Mixin Z2 Z2_pickle Z2_unpickle Z2_p_u_cancel.
-  Canonical Z2_countType := Eval hnf in CountType Z2 Z2_countMixin.
+  Definition Z2_hasCountable := isCountable.Build Z2 Z2_p_u_cancel.
+  HB.instance Definition _ := Z2_hasCountable.
 
   Definition Z2_enum : seq Z2 := [:: z; o].
   Lemma Z2_enum_uniq : uniq Z2_enum.
   Proof. reflexivity. Qed.
   Lemma mem_Z2_enum i : i \in Z2_enum.
   Proof. destruct i; reflexivity. Qed.
-  Definition Z2_finMixin :=
-    Eval hnf in UniqFinMixin Z2_enum_uniq mem_Z2_enum.
-  Canonical Z2_finType := Eval hnf in FinType Z2 Z2_finMixin.
+
+  Definition Z2_isFinite := isFinite.Build Z2 (Finite.uniq_enumP Z2_enum_uniq mem_Z2_enum).
+  HB.instance Definition _ := Z2_isFinite.
 
   Lemma assoc_add : associative add.
   Proof. move => [|] [|] [|] //. Qed.
@@ -75,16 +73,14 @@ Module Z2_manual.
   Lemma Z2_invgM : {morph inv : a b / add a b >-> add b a}.
   Proof. move => [|] [|] //. Qed.
 
-  Definition Z2_finGroupBaseMixin :=
-    FinGroup.BaseMixin assoc_add lid inv_inv Z2_invgM.
-
-  Canonical Z2_BaseFinGroupType :=
-    BaseFinGroupType Z2 Z2_finGroupBaseMixin.
+  Definition Z2_isMulBaseGroup := isMulBaseGroup.Build Z2 assoc_add lid inv_inv Z2_invgM.
+  HB.instance Definition _ := Z2_isMulBaseGroup.
 
   Definition linv : left_inverse z inv add.
   Proof. move => [|] //. Qed.
 
-  Canonical Z2_finGroup : finGroupType := FinGroupType linv.
+  Definition Z2_BaseFinGroup_isGroup := BaseFinGroup_isGroup.Build Z2 linv.
+  HB.instance Definition _ := Z2_BaseFinGroup_isGroup.
 
 End Z2_manual.
 
@@ -104,15 +100,15 @@ Module Z2_bool.
   Lemma bool_invgM : {morph invb : a b / addb a b >-> addb b a}.
   Proof. move => [|] [|] //. Qed.
 
-  Definition bool_finGroupBaseMixin :=
-    FinGroup.BaseMixin assoc_addb lidb inv_invb bool_invgM.
+  Definition bool_isMulBaseGroup := isMulBaseGroup.Build bool assoc_addb lidb inv_invb bool_invgM.
+  HB.instance Definition _ := bool_isMulBaseGroup.
 
-  Canonical bool_BaseFinGroupType :=
-    BaseFinGroupType bool bool_finGroupBaseMixin.
   Definition linvb : left_inverse false invb addb.
   Proof. move => [|] //. Qed.
 
-  Canonical bool_finGroup : finGroupType := FinGroupType linvb.
+  Definition bool_BaseFinGroup_isGroup := BaseFinGroup_isGroup.Build bool linvb.
+  HB.instance Definition _ := bool_BaseFinGroup_isGroup.
+
 End Z2_bool.
 
 Section Z3_deriving.
@@ -121,14 +117,23 @@ Section Z3_deriving.
 
   Definition Z3_indDef := [indDef for Z3_rect].
   Canonical Z3_indType := IndType Z3 Z3_indDef.
-  Definition Z3_eqMixin := [derive eqMixin for Z3].
-  Canonical Z3_eqType := EqType Z3 Z3_eqMixin.
-  Definition Z3_choiceMixin := [derive choiceMixin for Z3].
-  Canonical Z3_choiceType := ChoiceType Z3 Z3_choiceMixin.
-  Definition Z3_countMixin := [derive countMixin for Z3].
-  Canonical Z3_countType := CountType Z3 Z3_countMixin.
-  Definition Z3_finMixin := [derive finMixin for Z3].
-  Canonical Z3_finType := FinType Z3 Z3_finMixin.
+  Definition Z3_eqMixin := [derive hasDecEq for Z3].
+  HB.instance Definition _ := Z3_eqMixin.
+  Definition Z3_choiceMixin := [derive hasChoice for Z3].
+  HB.instance Definition _ := Z3_choiceMixin.
+  Definition Z3_countMixin := [derive isCountable for Z3].
+  HB.instance Definition _ := Z3_countMixin.
+  (* This does not work properly. Please check the output. *)
+  Definition Z3_finMixin := [derive isFinite for Z3].
+
+  (* Manual construction *)
+  Definition Z3_enum : seq Z3 := [:: z; o; t].
+  Lemma Z3_enum_uniq : uniq Z3_enum.
+  Proof. reflexivity. Qed.
+  Lemma mem_Z3_enum i : i \in Z3_enum.
+  Proof. destruct i; reflexivity. Qed.
+  Definition Z3_isFinite := isFinite.Build Z3 (Finite.uniq_enumP Z3_enum_uniq mem_Z3_enum).
+  HB.instance Definition _ := Z3_isFinite.
 
   Definition add (x y : Z3) : Z3 :=
     match x, y with
@@ -150,61 +155,12 @@ Section Z3_deriving.
   Lemma Z3_invgM : {morph inv : a b / add a b >-> add b a}.
   Proof. move => [||] [||] //. Qed.
 
-  Definition Z3_finGroupBaseMixin :=
-    FinGroup.BaseMixin assoc_add lid inv_inv Z3_invgM.
+  Definition Z3_finGroupBaseMixin := isMulBaseGroup.Build Z3 assoc_add lid inv_inv Z3_invgM.
 
-  Canonical Z3_BaseFinGroupType := BaseFinGroupType Z3 Z3_finGroupBaseMixin.
+  HB.instance Definition _ := Z3_finGroupBaseMixin.
   Definition linv : left_inverse z inv add.
   Proof. move => [||] //. Qed.
 
-  Canonical Z3_finGroup : finGroupType := FinGroupType linv.
+  Definition Z3_finGroup := BaseFinGroup_isGroup.Build Z3 linv.
+  HB.instance Definition _ := Z3_finGroup.
 End Z3_deriving.
-
-Module Z2.
-  (* Minimal (?) construction of Z2 using the fingroup mixin. *)
-  Definition invb x : bool := x.
-  Fact assoc_xorb : associative xorb.
-  Proof. move => [|] [|] [|] //. Qed.
-  Fact lidb : left_id false xorb.
-  Proof. move => [|] //. Qed.
-  Fact linvb : left_inverse false invb xorb.
-  Proof. move => [|] //. Qed.
-  Canonical bool_finGroup := BaseFinGroupType _ (FinGroup.Mixin assoc_xorb lidb linvb).
-  Canonical Z2_finGroup : finGroupType := FinGroupType linvb.
-End Z2.
-
-Module Z3.
-  (* Z3 using the fingroup mixin and deriving. *)
-  Inductive Z3 := z | o | t.
-
-  Definition Z3_indDef := [indDef for Z3_rect].
-  Canonical Z3_indType := IndType Z3 Z3_indDef.
-  Definition Z3_eqMixin := [derive eqMixin for Z3].
-  Canonical Z3_eqType := EqType Z3 Z3_eqMixin.
-  Definition Z3_choiceMixin := [derive choiceMixin for Z3].
-  Canonical Z3_choiceType := ChoiceType Z3 Z3_choiceMixin.
-  Definition Z3_countMixin := [derive countMixin for Z3].
-  Canonical Z3_countType := CountType Z3 Z3_countMixin.
-  Definition Z3_finMixin := [derive finMixin for Z3].
-  Canonical Z3_finType := FinType Z3 Z3_finMixin.
-
-  Definition add (x y : Z3) : Z3 :=
-    match x, y with
-    | z, _ => y
-    | _, z => x
-    | o, o => t
-    | o, t
-    | t, o => z
-    | t, t => o
-    end.
-  Definition inv x : Z3 := match x with o => t | t => o | z => z end.
-  Lemma assoc_add : associative add.
-  Proof. move => [||] [||] [||] //. Qed.
-  Lemma lid : left_id z add.
-  Proof. move => [||] //. Qed.
-  Lemma linv : left_inverse z inv add.
-  Proof. move => [||] //. Qed.
-
-  Canonical Z3_BaseFinGroupType := BaseFinGroupType _ (FinGroup.Mixin assoc_add lid linv).
-  Canonical Z3_finGroup : finGroupType := FinGroupType linv.
-End Z3.
diff --git a/theories/Crypt/examples/package_usage_example.v b/theories/Crypt/examples/package_usage_example.v
index 152c03ac..5e7928d8 100644
--- a/theories/Crypt/examples/package_usage_example.v
+++ b/theories/Crypt/examples/package_usage_example.v
@@ -59,10 +59,10 @@ Definition p1 : package fset0 [interface] I1 :=
     }
   ].
 
-Definition foo (x : bool) : code fset0 [interface] bool_choiceType :=
+Definition foo (x : bool) : code fset0 [interface] bool :=
   {code let u := x in ret u}.
 
-Definition bar (b : bool) : code fset0 [interface] nat_choiceType :=
+Definition bar (b : bool) : code fset0 [interface] nat :=
   {code if b then ret 0 else ret 1}.
 
 Definition p2 : package fset0 [interface] I2 :=
diff --git a/theories/Crypt/package/pkg_advantage.v b/theories/Crypt/package/pkg_advantage.v
index e17f21fe..42d42347 100644
--- a/theories/Crypt/package/pkg_advantage.v
+++ b/theories/Crypt/package/pkg_advantage.v
@@ -83,7 +83,7 @@ Definition Pr_op (p : raw_package) (o : opsig) (x : src o) :
 Arguments SDistr_bind {_ _}.
 
 Definition Pr (p : raw_package) :
-  SDistr (bool_choiceType) :=
+  SDistr (bool:choiceType) :=
   SDistr_bind
     (λ '(b, _), SDistr_unit _ b)
     (Pr_op p RUN Datatypes.tt empty_heap).
@@ -152,7 +152,7 @@ Qed. *)
   : package_scope. *)
 
 Definition state_pass_ {A} (p : raw_code A) :
-  heap_choiceType → raw_code (prod_choiceType A heap_choiceType).
+  heap_choiceType → raw_code (prod A heap_choiceType).
 Proof.
   induction p; intros h.
   - constructor.
@@ -369,7 +369,7 @@ Lemma Advantage_triangle :
 Proof.
   intros P Q R A.
   unfold AdvantageE.
-  apply ler_dist_add.
+  apply ler_distD.
 Qed.
 
 Fixpoint advantage_sum P l Q A :=
@@ -387,7 +387,7 @@ Proof.
   - simpl. auto.
   - simpl. eapply order.Order.POrderTheory.le_trans.
     + eapply Advantage_triangle.
-    + eapply ler_add.
+    + eapply lerD.
       * auto.
       * eapply ih.
 Qed.
@@ -429,7 +429,7 @@ Proof.
   intros Game_export F G H ε₁ ε₂ ε₃ h1 h2 h3 LA A vA hF hG hH.
   unfold adv_equiv in *.
   erewrite <- h1, <- h2, <- h3 by eassumption.
-  apply ler_dist_add.
+  apply ler_distD.
 Qed.
 
 Lemma Reduction :
diff --git a/theories/Crypt/package/pkg_composition.v b/theories/Crypt/package/pkg_composition.v
index aef005cf..b469896d 100644
--- a/theories/Crypt/package/pkg_composition.v
+++ b/theories/Crypt/package/pkg_composition.v
@@ -431,7 +431,7 @@ Section fset_par_facts.
       - cbn. symmetry. apply h. auto.
       - cbn. reflexivity.
     }
-    rewrite h1. reflexivity.
+    rewrite h1. rewrite eqseqE. by [apply/eqP/eqP].
   Qed.
 
 End fset_par_facts.
@@ -912,7 +912,7 @@ Proof.
 Qed.
 
 Lemma getm_def_in :
-  ∀ {A : eqType} n (x : A) (s : seq (nat_eqType * A)),
+  ∀ {A : eqType} n (x : A) (s : seq ((nat:eqType)%type * A)),
     getm_def s n = Some x →
     (n,x) \in s.
 Proof.
@@ -1106,4 +1106,4 @@ Proof.
     intro h. apply e.
     destruct h as [? h ?]. rewrite in_fset in h.
     eexists. all: eauto.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/Crypt/package/pkg_core_definition.v b/theories/Crypt/package/pkg_core_definition.v
index 6d128aae..b5b1e94f 100644
--- a/theories/Crypt/package/pkg_core_definition.v
+++ b/theories/Crypt/package/pkg_core_definition.v
@@ -15,7 +15,7 @@ Set Warnings "ambiguous-paths,notation-overridden,notation-incompatible-format".
 From extructures Require Import ord fset fmap.
 From Mon Require Import SPropBase.
 From Crypt Require Import Prelude Axioms ChoiceAsOrd RulesStateProb StateTransformingLaxMorph
-     choice_type.
+     choice_type Casts.
 
 Require Import Equations.Prop.DepElim.
 From Equations Require Import Equations.
diff --git a/theories/Crypt/package/pkg_distr.v b/theories/Crypt/package/pkg_distr.v
index ebbd1e59..f486dc16 100644
--- a/theories/Crypt/package/pkg_distr.v
+++ b/theories/Crypt/package/pkg_distr.v
@@ -87,7 +87,7 @@ Qed.
 
 Lemma card_prod_iprod :
   ∀ i j,
-    #|prod_finType (ordinal_finType i) (ordinal_finType j)| = (i * j)%N.
+    #|(prod (ordinal i:finType) (ordinal j:finType)) :finType| = (i * j)%N.
 Proof.
   intros i j.
   rewrite card_prod. simpl. rewrite !card_ord. reflexivity.
@@ -95,7 +95,7 @@ Qed.
 
 Definition ch2prod {i j} `{Positive i} `{Positive j}
   (x : Arit (uniform (i * j))) :
-  prod_choiceType (Arit (uniform i)) (Arit (uniform j)).
+  (Arit (uniform i)) * (Arit (uniform j)).
 Proof.
   simpl in *.
   eapply otf. rewrite card_prod_iprod.
@@ -103,7 +103,7 @@ Proof.
 Defined.
 
 Definition prod2ch {i j} `{Positive i} `{Positive j}
-  (x : prod_choiceType (Arit (uniform i)) (Arit (uniform j))) :
+  (x : (Arit (uniform i)) * (Arit (uniform j))) :
   Arit (uniform (i * j)).
 Proof.
   simpl in *.
@@ -114,7 +114,7 @@ Defined.
 
 Definition ch2prod_prod2ch :
   ∀ {i j} `{Positive i} `{Positive j}
-    (x : prod_choiceType (Arit (uniform i)) (Arit (uniform j))),
+    (x : (Arit (uniform i)) * (Arit (uniform j))),
     ch2prod (prod2ch x) = x.
 Proof.
   intros i j hi hj x.
@@ -148,7 +148,7 @@ Proof.
 Qed.
 
 Lemma ordinal_finType_inhabited :
-  ∀ i `{Positive i}, ordinal_finType i.
+  ∀ i `{Positive i}, (ordinal i :finType).
 Proof.
   intros i hi.
   exists 0%N. auto.
diff --git a/theories/Crypt/package/pkg_heap.v b/theories/Crypt/package/pkg_heap.v
index ed71ab8e..cc2c63c3 100644
--- a/theories/Crypt/package/pkg_heap.v
+++ b/theories/Crypt/package/pkg_heap.v
@@ -37,7 +37,7 @@ Set Primitive Projections.
 Definition pointed_value := ∑ (t : choice_type), t.
 
 Definition raw_heap := {fmap Location -> pointed_value}.
-Definition raw_heap_choiceType := [choiceType of raw_heap].
+Definition raw_heap_choiceType := Choice.clone _ raw_heap.
 
 Definition check_loc_val (l : Location) (v : pointed_value) :=
   l.π1 == v.π1.
@@ -67,7 +67,7 @@ Defined.
 
 Definition heap := { h : raw_heap | valid_heap h }.
 
-Definition heap_choiceType := [choiceType of heap].
+Definition heap_choiceType := Choice.clone _ heap.
 
 Lemma heap_ext :
   ∀ (h₀ h₁ : heap),
@@ -264,4 +264,4 @@ Proof.
   intros s ℓ v ℓ' v' ne.
   apply heap_ext. destruct s as [h vh]. simpl.
   apply setmC. auto.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/Crypt/package/pkg_invariants.v b/theories/Crypt/package/pkg_invariants.v
index aba4a0ff..05fa0d66 100644
--- a/theories/Crypt/package/pkg_invariants.v
+++ b/theories/Crypt/package/pkg_invariants.v
@@ -11,6 +11,9 @@ Set Warnings "-ambiguous-paths,-notation-overridden,-notation-incompatible-forma
 From mathcomp Require Import ssrnat ssreflect ssrfun ssrbool ssrnum eqtype
   choice reals distr seq all_algebra fintype realsum.
 Set Warnings "ambiguous-paths,notation-overridden,notation-incompatible-format".
+
+From HB Require Import structures.
+
 From extructures Require Import ord fset fmap.
 From Mon Require Import SPropBase.
 From Crypt Require Import Prelude Axioms ChoiceAsOrd SubDistr Couplings
@@ -905,9 +908,12 @@ Proof.
   all: intro h. all: inversion h. all: contradiction.
 Qed.
 
-Canonical heap_val_eqMixin := EqMixin heap_val_eqP.
+(*Canonical heap_val_eqMixin := EqMixin heap_val_eqP.
 Canonical heap_val_eqType :=
-  Eval hnf in EqType heap_val heap_val_eqMixin.
+  Eval hnf in EqType heap_val heap_val_eqMixin. *)
+Definition heap_val_hasDecEq := hasDecEq.Build heap_val heap_val_eqP.
+HB.instance Definition _ := heap_val_hasDecEq.
+
 
 Derive NoConfusion for heap_val.
 
@@ -1598,4 +1604,4 @@ Proof.
     specialize ih with (1 := h).
     specialize ih with (1 := hh).
     rewrite e in ih. apply ih.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/Crypt/package/pkg_rhl.v b/theories/Crypt/package/pkg_rhl.v
index 38dc5949..b3393a5a 100644
--- a/theories/Crypt/package/pkg_rhl.v
+++ b/theories/Crypt/package/pkg_rhl.v
@@ -18,7 +18,7 @@ From Crypt Require Import Prelude Axioms ChoiceAsOrd SubDistr Couplings
   RulesStateProb UniformStateProb UniformDistrLemmas StateTransfThetaDens
   StateTransformingLaxMorph choice_type pkg_core_definition pkg_notation
   pkg_tactics pkg_composition pkg_heap pkg_semantics pkg_lookup pkg_advantage
-  pkg_invariants pkg_distr.
+  pkg_invariants pkg_distr Casts.
 Require Import Equations.Prop.DepElim.
 From Equations Require Import Equations.
 
@@ -166,7 +166,9 @@ Proof.
   match goal with
   | |- realsum.summable ?f => eassert (f = _) as Hf end.
   { extensionality x.
-    apply (destruct_pair_eq (a:= f1 x) (b:=f3 x) (c:= f2 x) (d := f4 x)). }
+    instantiate (1 := fun x1 => (f1 x1 == f3 x1)%:R * (f2 x1 == f4 x1)%:R).
+    simpl.
+    exact: (destruct_pair_eq (a:= f1 x) (b:=f3 x) (c:= f2 x) (d := f4 x)). }
   rewrite Hf.
   apply realsum.summableM. all: assumption.
 Qed.
@@ -2133,7 +2135,8 @@ Section Uniform_prod.
       destruct (ch2prod u == (a,b)) eqn:e.
       2:{
         exfalso.
-        move: hu => /negP hu. apply hu. apply eqxx.
+        move: hu => /negP hu. apply hu.
+        by [rewrite e].
       }
       move: e => /eqP e. rewrite -e.
       rewrite inE. apply /eqP. symmetry. apply prod2ch_ch2prod.
@@ -2184,7 +2187,7 @@ Section Uniform_prod.
     eapply rewrite_eqDistrR. 1: apply: reflexivity_rule.
     intro s. cbn.
     pose proof @prod_uniform as h.
-    specialize (h [finType of 'I_i] [finType of 'I_j]). simpl in h.
+    specialize (h (Finite.clone _ 'I_i) (Finite.clone _ 'I_j)). simpl in h.
     unfold Uni_W'. unfold Uni_W.
     specialize (h (F_w0 (mkpos _)) (F_w0 (mkpos _))).
     unfold uniform_F in h.
diff --git a/theories/Crypt/rhl_semantics/ChoiceAsOrd.v b/theories/Crypt/rhl_semantics/ChoiceAsOrd.v
index 97ce586c..1e59e3cb 100644
--- a/theories/Crypt/rhl_semantics/ChoiceAsOrd.v
+++ b/theories/Crypt/rhl_semantics/ChoiceAsOrd.v
@@ -1,5 +1,6 @@
 From Mon Require Import SPropBase.
 From Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples.
+From Crypt Require Import Casts.
 Set Warnings "-notation-overridden".
 From mathcomp Require Import all_ssreflect.
 Set Warnings "notation-overridden".
@@ -32,8 +33,6 @@ Program Definition choice_incl := @mkOrdFunctor ord_choiceType TypeCat
     (fun (A:ord_choiceType) => A)
     (fun (A B : ord_choiceType) f => f)
     _ _ _.
-  Next Obligation. cbv ; intuition. Qed.
-
 
 
 Section Prod_of_choiceTypes.
diff --git a/theories/Crypt/rhl_semantics/only_prob/Theta_exCP.v b/theories/Crypt/rhl_semantics/only_prob/Theta_exCP.v
index fd4a705e..a9275d9d 100644
--- a/theories/Crypt/rhl_semantics/only_prob/Theta_exCP.v
+++ b/theories/Crypt/rhl_semantics/only_prob/Theta_exCP.v
@@ -3,7 +3,8 @@ From mathcomp Require Import all_ssreflect all_algebra boolp distr reals realsum
 Set Warnings "notation-overridden,ambiguous-paths".
 From Mon Require Import SpecificationMonads SPropBase SPropMonadicStructures.
 From Relational Require Import OrderEnrichedCategory OrderEnrichedRelativeMonadExamples.
-From Crypt Require Import ChoiceAsOrd SubDistr Couplings Axioms.
+From Crypt Require Import ChoiceAsOrd SubDistr Couplings Axioms Casts.
+From HB Require Import structures.
 
 Import SPropNotations.
 Import Num.Theory.
@@ -91,9 +92,7 @@ Proof.
     apply: boolp.funext. by move => [c1 c2] /=.
 Defined.
 
-
-
-Definition θ0 (A1 A2 : Type) (ch1 : Choice.class_of A1) (ch2 : Choice.class_of A2):
+Definition θ0 (A1 A2 : Type) (ch1 : Choice A1) (ch2 : Choice A2):
   (SDistr_carrier (Choice.Pack ch1)) × (SDistr_carrier (Choice.Pack ch2)) ->
   WProp (A1 * A2)%type.
 Proof.
@@ -116,8 +115,8 @@ Proof.
   inversion leq12. by subst.
 Defined.
 
-Definition kd {A1 A2 B1 B2 : Type} {chA1 : Choice.class_of A1} {chA2 : Choice.class_of A2}
-                                   {chB1 : Choice.class_of B1} {chB2 : Choice.class_of B2}
+Definition kd {A1 A2 B1 B2 : Type} {chA1 : Choice A1} {chA2 : Choice A2}
+                                   {chB1 : Choice B1} {chB2 : Choice B2}
               {f1 : TypeCat ⦅ nfst (prod_functor choice_incl choice_incl ⟨
                                Choice.Pack chA1, Choice.Pack chA2 ⟩);
                               nfst (SDistr_squ ⟨Choice.Pack chB1, Choice.Pack chB2 ⟩) ⦆}
@@ -151,7 +150,7 @@ Proof.
   - exists dnull. intro. inversion H.
 Defined.
 
-Lemma extract_positive : forall {A1 A2 B1 B2 : Type} {chA1 : Choice.class_of A1} {chA2 : Choice.class_of A2} {chB1 : Choice.class_of B1} {chB2 : Choice.class_of B2}  (dA : SDistr_carrier (F_choice_prod_obj ⟨ Choice.Pack chA1, Choice.Pack chA2 ⟩)) (FF1 : _ -> SDistr (F_choice_prod ⟨ Choice.Pack chB1, Choice.Pack chB2 ⟩)) b1 b2, 0 < (\dlet_(i <- dA) (FF1 i)) (b1, b2) -> exists (a1 : Choice.Pack chA1) (a2 : Choice.Pack chA2), 0 < dA (a1, a2) /\ 0 < FF1 (a1, a2) (b1, b2).
+Lemma extract_positive : forall {A1 A2 B1 B2 : Type} {chA1 : Choice A1} {chA2 : Choice A2} {chB1 : Choice B1} {chB2 : Choice B2}  (dA : SDistr_carrier (F_choice_prod_obj ⟨ Choice.Pack chA1, Choice.Pack chA2 ⟩)) (FF1 : _ -> SDistr (F_choice_prod ⟨ Choice.Pack chB1, Choice.Pack chB2 ⟩)) b1 b2, 0 < (\dlet_(i <- dA) (FF1 i)) (b1, b2) -> exists (a1 : Choice.Pack chA1) (a2 : Choice.Pack chA2), 0 < dA (a1, a2) /\ 0 < FF1 (a1, a2) (b1, b2).
 Proof.
   intuition. rewrite /(\dlet_(i <- _) _) in H. unlock in H. simpl in H.
   rewrite /mlet in H.
@@ -174,7 +173,7 @@ Proof.
     apply FF1z.
 Qed.
 
-Lemma distr_get : forall {A : Type} {chA : Choice.class_of A} x y, 0 < SDistr_unit (Choice.Pack chA) x y -> x = y.
+Lemma distr_get : forall {A : Type} {chA : Choice A} x y, 0 < SDistr_unit (Choice.Pack chA) x y -> x = y.
 Proof.
   intuition. rewrite /SDistr_unit in H. rewrite dunit1E in H.
   case Hxy: (x==y).
@@ -274,7 +273,7 @@ Definition flip (r : R) : SDistr (bool_choiceType).
   - exact (1 - r).
 Defined.
 
-Lemma sample_rule : forall {A1 A2} {chA1 : Choice.class_of A1} {chA2 : Choice.class_of A2}
+Lemma sample_rule : forall {A1 A2} {chA1 : Choice A1} {chA2 : Choice A2}
                       (pre : Prop) (post : A1 -> A2 -> Prop)
                       (d1 : SDistr (Choice.Pack chA1)) (d2 : SDistr (Choice.Pack chA2)) d
                       (Hd : coupling d d1 d2)
@@ -298,7 +297,7 @@ Qed.
 
 (* GENERIC MONADIC RULES *)
 
-Theorem ret_rule  {A1 A2 : Type} {chA1 : Choice.class_of A1} {chA2 : Choice.class_of A2}
+Theorem ret_rule  {A1 A2 : Type} {chA1 : Choice A1} {chA2 : Choice A2}
                   (a1 : A1) (a2 : A2) :
 
    ⊨ (ord_relmon_unit SDistr (Choice.Pack chA1) a1) ≈
@@ -317,7 +316,7 @@ Proof.
     by rewrite -(distr_get _ _ Hb1b2).
 Qed.
 
-Theorem weaken_rule  {A1 A2 : Type} {chA1 : Choice.class_of A1} {chA2 : Choice.class_of A2}
+Theorem weaken_rule  {A1 A2 : Type} {chA1 : Choice A1} {chA2 : Choice A2}
                      {d1 : SDistr (Choice.Pack chA1)}
                      {d2 : SDistr (Choice.Pack chA2)} :
   forall w w', (⊨ d1 ≈ d2 [{ w }]) -> w ≤ w' -> (⊨ d1 ≈ d2 [{ w' }] ).
diff --git a/theories/Crypt/rhl_semantics/state_prob/StateTransformingLaxMorph.v b/theories/Crypt/rhl_semantics/state_prob/StateTransformingLaxMorph.v
index d3082192..6db7e7aa 100644
--- a/theories/Crypt/rhl_semantics/state_prob/StateTransformingLaxMorph.v
+++ b/theories/Crypt/rhl_semantics/state_prob/StateTransformingLaxMorph.v
@@ -5,7 +5,7 @@ From Mon Require Import SPropBase.
 Set Warnings "-notation-overridden,-ambiguous-paths".
 From mathcomp Require Import all_ssreflect (*boolp*).
 Set Warnings "notation-overridden,ambiguous-paths".
-From Crypt Require Import Axioms OrderEnrichedRelativeAdjunctions LaxFunctorsAndTransf LaxMorphismOfRelAdjunctions TransformingLaxMorph OrderEnrichedRelativeAdjunctionsExamples ThetaDex SubDistr Theta_exCP ChoiceAsOrd FreeProbProg UniversalFreeMap RelativeMonadMorph_prod LaxComp choice_type.
+From Crypt Require Import Axioms OrderEnrichedRelativeAdjunctions LaxFunctorsAndTransf LaxMorphismOfRelAdjunctions TransformingLaxMorph OrderEnrichedRelativeAdjunctionsExamples ThetaDex SubDistr Theta_exCP ChoiceAsOrd FreeProbProg UniversalFreeMap RelativeMonadMorph_prod LaxComp choice_type Casts.
 (* From Crypt Require Import only_prob.Rules. *)
 
 Import SPropNotations.
diff --git a/theories/Crypt/rules/RulesProb.v b/theories/Crypt/rules/RulesProb.v
index cc4ff566..c65e13ae 100644
--- a/theories/Crypt/rules/RulesProb.v
+++ b/theories/Crypt/rules/RulesProb.v
@@ -31,7 +31,8 @@ From Crypt Require Import
      Theta_exCP
      LaxComp
      FreeProbProg
-     RelativeMonadMorph_prod.
+     RelativeMonadMorph_prod
+     Casts.
 
 Import SPropNotations.
 Import Num.Theory.
@@ -162,7 +163,7 @@ Definition get_d { A  : choiceType} (c : MFreePr A):=
   (Theta_dens.unary_theta_dens_obligation_1 A c).
 
 Lemma sample_rule :
-  ∀ {A1 A2} {chA1 : Choice.class_of A1} {chA2 : Choice.class_of A2}
+  ∀ {A1 A2} {chA1 : Choice A1} {chA2 : Choice A2}
     (pre : Prop) (post : A1 -> A2 -> Prop)
     (c1 : MFreePr (Choice.Pack chA1))
     (c2 : MFreePr (Choice.Pack chA2))
@@ -205,7 +206,7 @@ Qed.
 (* GENERIC MONADIC RULES *)
 
 Theorem ret_ule {A1 A2 : Type}
-  {chA1 : Choice.class_of A1} {chA2 : Choice.class_of A2}
+  {chA1 : Choice A1} {chA2 : Choice A2}
   (a1 : A1) (a2 : A2) :
    ⊨ (ord_relmon_unit MFreePr (Choice.Pack chA1) a1) ≈
      (ord_relmon_unit MFreePr (Choice.Pack chA2) a2)
@@ -229,7 +230,7 @@ Proof.
   by apply: ret_rule.
 Qed.
 
-Theorem weaken_rule  {A1 A2 : Type} {chA1 : Choice.class_of A1} {chA2 : Choice.class_of A2}
+Theorem weaken_rule  {A1 A2 : Type} {chA1 : Choice A1} {chA2 : Choice A2}
                      {d1 : MFreePr (Choice.Pack chA1)}
                      {d2 : MFreePr (Choice.Pack chA2)} :
   forall w w', (⊨ d1 ≈ d2 [{ w }]) -> w ≤ w' -> (⊨ d1 ≈ d2 [{ w' }] ).
@@ -243,8 +244,8 @@ Proof.
 Qed.
 
 
-Theorem bind_rule {A1 A2 : Type} {chA1 : Choice.class_of A1} {chA2 : Choice.class_of A2}
-                  {B1 B2 : Type} {chB1 : Choice.class_of B1} {chB2 : Choice.class_of B2}
+Theorem bind_rule {A1 A2 : Type} {chA1 : Choice A1} {chA2 : Choice A2}
+                  {B1 B2 : Type} {chB1 : Choice B1} {chB2 : Choice B2}
                   {f1 : A1 -> MFreePr (Choice.Pack chB1)}
                   {f2 : A2 -> MFreePr (Choice.Pack chB2)}
                   (m1 : MFreePr (Choice.Pack chA1))
@@ -278,7 +279,7 @@ Qed.
 
 (* Pre-condition manipulating rules *)
 
-Theorem pre_weaken_rule  {A1 A2 : Type} {chA1 : Choice.class_of A1} {chA2 : Choice.class_of A2}
+Theorem pre_weaken_rule  {A1 A2 : Type} {chA1 : Choice A1} {chA2 : Choice A2}
                         {d1 : MFreePr (Choice.Pack chA1)}
                         {d2 : MFreePr (Choice.Pack chA2)} :
   forall (pre pre' : Prop) post, (⊨ ⦃ pre ⦄ d1 ≈ d2 ⦃ post ⦄) -> (pre' -> pre) -> (⊨ ⦃ pre' ⦄ d1 ≈ d2 ⦃ post ⦄).
@@ -291,7 +292,7 @@ Proof.
   simpl; intuition.
 Qed.
 
-Theorem pre_hypothesis_rule  {A1 A2 : Type} {chA1 : Choice.class_of A1} {chA2 : Choice.class_of A2}
+Theorem pre_hypothesis_rule  {A1 A2 : Type} {chA1 : Choice A1} {chA2 : Choice A2}
                         {d1 : MFreePr (Choice.Pack chA1)}
                         {d2 : MFreePr (Choice.Pack chA2)} :
   forall (pre : Prop) post, (pre -> ⊨ ⦃ True ⦄ d1 ≈ d2 ⦃ post ⦄) -> (⊨ ⦃ pre ⦄ d1 ≈ d2 ⦃ post ⦄).
@@ -323,7 +324,7 @@ Qed.
 
 (* post-condition manipulating rules *)
 
-Theorem post_weaken_rule  {A1 A2 : Type} {chA1 : Choice.class_of A1} {chA2 : Choice.class_of A2}
+Theorem post_weaken_rule  {A1 A2 : Type} {chA1 : Choice A1} {chA2 : Choice A2}
         {d1 : MFreePr (Choice.Pack chA1)}
         {d2 : MFreePr (Choice.Pack chA2)} :
   forall (pre : Prop) (post1 post2 : A1 -> A2 -> Prop),
@@ -438,7 +439,7 @@ Proof. by  apply: (seq_rule_ch m1 m2 P (fun _ _ => True) Q judge1 judge2). Qed.
 
 (* *)
 
-Theorem if_rule  {A1 A2 : Type} {chA1 : Choice.class_of A1} {chA2 : Choice.class_of A2}
+Theorem if_rule  {A1 A2 : Type} {chA1 : Choice A1} {chA2 : Choice A2}
         (c1 c2 : MFreePr (Choice.Pack chA1))
         (c1' c2' : MFreePr (Choice.Pack chA2))
         {b1 b2 : bool}
@@ -463,7 +464,7 @@ Proof.
   - intuition.
 Qed.
 
-Theorem if_rule_weak  {A1 A2 : Type} {chA1 : Choice.class_of A1} {chA2 : Choice.class_of A2}
+Theorem if_rule_weak  {A1 A2 : Type} {chA1 : Choice A1} {chA2 : Choice A2}
         (c1 c2 : MFreePr (Choice.Pack chA1))
         (c1' c2' : MFreePr (Choice.Pack chA2))
         {b : bool}
@@ -485,7 +486,7 @@ Axiom s_indefinite_description :
 
 
 
-Definition judgement_d {A1 A2 : Type} {chA1 : Choice.class_of A1} {chA2 : Choice.class_of A2}
+Definition judgement_d {A1 A2 : Type} {chA1 : Choice A1} {chA2 : Choice A2}
            {c1 : MFreePr (Choice.Pack chA1)}
            {c2 : MFreePr (Choice.Pack chA2)}
            {pre : Prop} {post : A1 -> A2 -> Prop}
@@ -548,7 +549,7 @@ Fixpoint bounded_do_while  (n : nat) (c : MFreePr bool_choiceType) :
 
 (* Rem.: maybe something like the rule in the paper can be proven? yes...
        but I do not have intuition of how it could be used... examples needed! *)
-Theorem bounded_do_while_rule  {A1 A2 : Type} {chA1 : Choice.class_of A1} {chA2 : Choice.class_of A2} {n : nat}
+Theorem bounded_do_while_rule  {A1 A2 : Type} {chA1 : Choice A1} {chA2 : Choice A2} {n : nat}
         (c1 c2 : MFreePr bool_choiceType)
         {inv : bool -> bool -> Prop}
         {H : ⊨ ⦃ inv true true ⦄ c1 ≈ c2 ⦃ fun b1 b2 => inv b1 b2 /\ b1 = b2 ⦄ } :
@@ -747,7 +748,7 @@ Proof.
            by move/orP: Hd0. }
        --- move/eqP : Hdor1 => Hdor1.
            by rewrite -Hdor1 !GRing.mulr0.
-       --- apply: ler_pmul.
+       --- apply: ler_pM.
            + case: (A x1); rewrite //=; exact ler01.
            + by inversion d.
            + move:  (H2 x1 x2 Hdor2) => HAB.
diff --git a/theories/Crypt/rules/RulesStateProb.v b/theories/Crypt/rules/RulesStateProb.v
index 4374d492..d14e9b25 100644
--- a/theories/Crypt/rules/RulesStateProb.v
+++ b/theories/Crypt/rules/RulesStateProb.v
@@ -8,16 +8,18 @@ From Relational Require Import OrderEnrichedCategory
 
 Set Warnings "-notation-overridden,-ambiguous-paths".
 From mathcomp Require Import all_ssreflect all_algebra reals distr realsum
-  finmap.set finmap.finmap xfinmap.
+  finset finmap.finmap xfinmap .
 Set Warnings "notation-overridden,ambiguous-paths".
 
 From Crypt Require Import Axioms ChoiceAsOrd SubDistr Couplings Theta_dens
   Theta_exCP LaxComp FreeProbProg RelativeMonadMorph_prod
-  StateTransformingLaxMorph choice_type.
+  StateTransformingLaxMorph choice_type Casts.
 
 Import SPropNotations.
 Import Num.Theory.
 
+From HB Require Import structures.
+
 
 #[local] Open Scope ring_scope.
 
@@ -126,7 +128,7 @@ End RSemanticNotation.
 Import RSemanticNotation.
 #[local] Open Scope rsemantic_scope.
 
-Import finmap.set finmap.finmap xfinmap.
+Import (* finmap.set *) finset finmap.finmap xfinmap.
 
 Open Scope fset_scope.
 
@@ -784,7 +786,7 @@ Proof.
   clear Hpsum.
   eapply neq0_psum in Hpsum'. destruct Hpsum'.
   apply aux_domain in H.
-  destruct (eqType_lem  bool_eqType ((x,x) == (a1,a2)) true) as [Houi | Hnon].
+  destruct (eqType_lem  _ ((x,x) == (a1,a2)) true) as [Houi | Hnon].
   move: Houi => /eqP Houi. move: Houi => [H1 H2]. rewrite -H1 -H2. reflexivity.
   have Hnon' : (x,x) == (a1,a2) = false.
     destruct ((x,x) == (a1,a2)). contradiction. reflexivity.
@@ -807,19 +809,16 @@ Qed.
 
 Definition dsym { A B : ord_choiceType } { S1 S2 : choiceType } (d : SDistr_carrier
           (F_choice_prod_obj
-             ⟨ Choice.Pack {| Choice.base := prod_eqMixin B S2; Choice.mixin := prod_choiceMixin B S2 |},
-               Choice.Pack {| Choice.base := prod_eqMixin A S1; Choice.mixin := prod_choiceMixin A S1 |} ⟩)) :
+             ⟨ ((B * S2)%type : choiceType), ((A * S1)%type : choiceType) ⟩)) :
 SDistr_carrier
           (F_choice_prod_obj
-             ⟨ Choice.Pack {| Choice.base := prod_eqMixin A S1; Choice.mixin := prod_choiceMixin A S1 |},
-               Choice.Pack {| Choice.base := prod_eqMixin B S2; Choice.mixin := prod_choiceMixin B S2 |} ⟩) :=
+             ⟨ ((A * S1)%type : choiceType), ((B * S2)%type : choiceType) ⟩) :=
 dswap d.
 
 
 Lemma dsym_coupling { A B : ord_choiceType } { S1 S2 : choiceType } { d : SDistr_carrier
           (F_choice_prod_obj
-             ⟨ Choice.Pack {| Choice.base := prod_eqMixin B S2; Choice.mixin := prod_choiceMixin B S2 |},
-               Choice.Pack {| Choice.base := prod_eqMixin A S1; Choice.mixin := prod_choiceMixin A S1 |} ⟩) }
+             ⟨ ((B * S2)%type : choiceType), ((A * S1)%type : choiceType) ⟩) }
       {d1 d2 }
       (Hcoupling : coupling d d1 d2) : coupling (dsym d) d2 d1.
 Proof.
@@ -1597,8 +1596,8 @@ Proof.
   apply mulr_ge0.
   destruct q as [qmap q_0 q_sum q_1]. apply q_0.
   easy.
-(* ler_pimulr: forall [R : numDomainType] [x y : R], 0 <= y -> x <= 1 -> y * x <= y *)
-  apply ler_pimulr. destruct q as [qmap q_0 q_sum q_1]. apply q_0.
+(* ler_piMr: forall [R : numDomainType] [x y : R], 0 <= y -> x <= 1 -> y * x <= y *)
+  apply ler_piMr. destruct q as [qmap q_0 q_sum q_1]. apply q_0.
   apply le1_mu1. easy. destruct q as [qmap q_0 q_sum q_1]. apply q_1.
 Qed.
 
diff --git a/theories/Crypt/rules/UniformDistrLemmas.v b/theories/Crypt/rules/UniformDistrLemmas.v
index a051ac4a..95bdd3b9 100644
--- a/theories/Crypt/rules/UniformDistrLemmas.v
+++ b/theories/Crypt/rules/UniformDistrLemmas.v
@@ -31,7 +31,8 @@ From Crypt Require Import
      Theta_dens
      Theta_exCP
      LaxComp
-     FreeProbProg.
+     FreeProbProg
+     Casts.
 
 Import SPropNotations.
 Import Num.Theory.
@@ -61,16 +62,15 @@ Qed.
 
 (* Rem.: TODO: generalize this *)
 Lemma sum_const_seq_finType { T : finType } ( J : seq T) (k : R) (Huniq : uniq J) :
-  \sum_(j <- J) k = \sum_(j in (seq_sub_finType J)) k.
+  \sum_(j <- J) k = \sum_(j in J) k.
 Proof.
-  rewrite /seq_sub_finType. simpl.
   rewrite big_const.
   rewrite big_const_seq.
-  rewrite card_seq_sub.
-  - simpl.
-    rewrite count_predT.
-    reflexivity.
-  - apply Huniq.
+  f_equal.
+  rewrite count_predT.
+  apply esym.
+  apply/card_uniqP.
+  exact: Huniq.
 Qed.
 
 
@@ -81,16 +81,16 @@ Proof.
   rewrite sum_const_seq_finType.
   2: { exact Huniq. }
   rewrite GRing.sumr_const pmulrn /=.
-  have hfoo' :  k *~ #|seq_sub_finType (T:=T) J| =  k * #|seq_sub_finType (T:=T) J|%:~R.
-  { by rewrite mulrzr. }
+  have hfoo' :  k *~ #|J| =  k * #|J|%:~R.
+  1: { by rewrite mulrzr. }
   rewrite hfoo' /=.
-  apply: ler_pmul; auto.
-  - rewrite ler0z. rewrite lez_nat. reflexivity.
-  - rewrite card_seq_sub. 2: eauto.
-    rewrite cardT.
-    rewrite ler_int. rewrite lez_nat.
-    rewrite uniq_leq_size. 1,2: auto.
-    intros x hx.
+  clear hfoo'.
+  apply: ler_pM; auto.
+  rewrite cardT.
+  rewrite ler_int. rewrite lez_nat.
+  rewrite cardE. apply uniq_leq_size.
+  - apply: enum_uniq.
+  - intros x hx.
     rewrite mem_enum. reflexivity.
 Qed.
 
@@ -104,7 +104,7 @@ Proof.
   (* Basically a rip-off of xfinmap.big_fset_subset *)
   intros T J hu π hπ.
   rewrite [X in _<=X](bigID [pred j : T | j \in J]) /=.
-  rewrite ler_paddr ?sumr_ge0 // -[X in _<=X]big_filter.
+  rewrite ler_wpDr ?sumr_ge0 // -[X in _<=X]big_filter.
   rewrite Order.POrderTheory.le_eqVlt; apply/orP; left; apply/eqP/perm_big.
   apply/uniq_perm; rewrite ?filter_uniq //; last move=> i.
   rewrite -enum_setT. apply enum_uniq.
@@ -225,12 +225,9 @@ Proof.
   rewrite GRing.mulrC.
   rewrite GRing.Theory.mulr_natl.
   apply f_equal.
-  rewrite card_seq_sub.
-  + rewrite cardE.
-    rewrite -enumT.
-    reflexivity.
-  + rewrite -enumT.
-    apply enum_uniq.
+  rewrite -enumT. rewrite [RHS]cardE.
+  apply: eq_cardT.
+  apply: mem_enum.
 Qed.
 
 (* the uniform distribution over F *)
diff --git a/theories/Crypt/rules/UniformStateProb.v b/theories/Crypt/rules/UniformStateProb.v
index b221c41d..d4f8c044 100644
--- a/theories/Crypt/rules/UniformStateProb.v
+++ b/theories/Crypt/rules/UniformStateProb.v
@@ -22,7 +22,7 @@ Local Open Scope ring_scope.
 
 Definition Index : Type := positive.
 
-Definition fin_family (i : Index) : finType := [finType of chFin i].
+Definition fin_family (i : Index) : finType := Finite.clone _ (chFin i).
 
 Lemma F_w0 :
   forall (i : Index), fin_family i.
@@ -117,7 +117,8 @@ Proof.
     rewrite Heq'. rewrite GRing.mulr1. reflexivity.
   - have Heq' : st == s = false. apply /eqP. move /eqP: Heq. congruence.
     rewrite Heq'. rewrite GRing.mulr0. reflexivity.
-  Unshelve. exact (Real.ringType R).
+    Unshelve.
+    exact: R.
 Qed.
 
 Definition f_dprod { F1 F2: finType } { S1 S2 : choiceType } { w0 : F1 } { w0' : F2 } {s1 : S1 } {s2 : S2}
@@ -218,7 +219,7 @@ Proof.
     rewrite item_addr0_mulr.
     eapply Order.POrderTheory.le_trans with (y := @r _ w0 *~ #|F1|).
     + rewrite -mulrzr. rewrite -[X in _<=X]mulrzr.
-      rewrite ler_pmul2l.
+      rewrite ler_pM2l.
       * rewrite ler_int. auto.
       * unfold r. apply mulr_gt0.
         -- cbn. rewrite ltr01. reflexivity.
@@ -232,17 +233,18 @@ Proof.
               destruct #|F1| eqn:e. 1: contradiction.
               rewrite ltr0n. reflexivity.
     + unfold r. rewrite -[X in X <= _]mulrzr. rewrite GRing.div1r.
-      erewrite <- GRing.mulr1. rewrite -GRing.mulrA.
+      rewrite -[X in X <= _]GRing.mulr1 -GRing.mulrA.
       rewrite GRing.Theory.mulKf.
       * auto.
       * unshelve eapply card_non_zero. auto.
 Qed.
 
+
 Definition UniformFsq_f { F1 F2 : finType} { w0 : F1 } { w0' : F2 }
                         { S1 S2 : choiceType } { s1 : S1 } { s2 : S2 }
                         {f : F1 -> F2} (f_bij : bijective f):
-  SDistr (ChoiceAsOrd.F_choice_prod ⟨ ChoiceAsOrd.F_choice_prod ⟨ Finite.choiceType F1 , S1 ⟩ ,
-                                    ChoiceAsOrd.F_choice_prod ⟨ Finite.choiceType F2 , S2 ⟩ ⟩ ).
+  SDistr (ChoiceAsOrd.F_choice_prod ⟨ ChoiceAsOrd.F_choice_prod ⟨ (F1:choiceType) , S1 ⟩ ,
+                                    ChoiceAsOrd.F_choice_prod ⟨ (F2:choiceType) , S2 ⟩ ⟩ ).
 Proof.
   unshelve eapply mkdistr.
   1:{
diff --git a/theories/Mon/FiniteProbabilities.v b/theories/Mon/FiniteProbabilities.v
index c0fdb857..c9311c9d 100644
--- a/theories/Mon/FiniteProbabilities.v
+++ b/theories/Mon/FiniteProbabilities.v
@@ -54,8 +54,8 @@ Section FinProb.
   Next Obligation.
     intros x y. simpl.
     rewrite divr_ge0 ?Bool.andb_true_l ?ler0n ?addr_ge0 //.
-    rewrite ler_pdivr_mulr.
-    rewrite mul1r [2%:~R]/(1+1) ler_add //.
+    rewrite ler_pdivrMr.
+    rewrite mul1r [2%:~R]/(1+1) lerD //.
     rewrite ltr0n //.
   Qed.
 
@@ -64,13 +64,13 @@ Section FinProb.
     intros. simpl.
     rewrite mulr_ge0 //=.
     rewrite -{3}(mul1r 1).
-    rewrite ler_pmul //=.
+    rewrite ler_pM //=.
   Qed.
 
   #[program] Definition negI (x:I) : I := ⦑ 1 - x∙1 ⦒.
   Next Obligation.
     intros. simpl.
-    rewrite subr_ge0 (I_le1 x) /= ler_subl_addr -{1}(addr0 1) ler_add ?lerr //.
+    rewrite subr_ge0 (I_le1 x) /= lerBlDr -{1}(addr0 1) lerD ?lerr //.
   Qed.
 
   Definition ProbS := I.
@@ -86,7 +86,7 @@ Section FinProb.
     rewrite addr_ge0 ?mulr_ge0 //.
     have: (1 = p∙1*1 + (1 - p∙1)*1) by rewrite !mulr1 addrA [_+1]addrC addrK.
     move=> heq; rewrite [X in _ <= X]heq.
-    by rewrite ler_add // ler_pmul // (I_ge0 (negI p)).
+    by rewrite lerD // ler_pM // (I_ge0 (negI p)).
   Qed.
 
   #[program] Definition wopProb (p:ProbS) : WI (ProbAr p) :=
@@ -94,7 +94,7 @@ Section FinProb.
   Next Obligation.
     intros p ? ? H.
     rewrite /Irel /=.
-    rewrite ler_add // ler_pmul //; try by apply H.
+    rewrite lerD // ler_pM //; try by apply H.
     by rewrite (I_ge0 (negI p)).
   Qed.
 
diff --git a/theories/Mon/Monoid.v b/theories/Mon/Monoid.v
index bfeb9518..781c4c40 100644
--- a/theories/Mon/Monoid.v
+++ b/theories/Mon/Monoid.v
@@ -62,7 +62,7 @@ Section MonoidExamples.
   Next Obligation. extensionality y ; rewrite monoid_law3 //. Qed.
 
   Program Definition listMonoid (X:Type) : monoid :=
-    @mkMonoid (list X) nil (@app _) _ (@List.app_nil_r _) (@List.app_assoc_reverse _).
+    @mkMonoid (list X) nil (@app _) _ (@List.app_nil_r _) (fun l m n => eq_sym (@List.app_assoc _ l m n)).
 
   Program Definition prodMonoid (M1 M2:monoid) : monoid :=
     @mkMonoid (M1 × M2) ⟨e M1, e M2⟩ (fun x y => ⟨nfst x ⋅ nfst y, nsnd x ⋅ nsnd y⟩)