diff --git a/coq-itree-extra.opam b/coq-itree-extra.opam
index 71a36057..12508566 100644
--- a/coq-itree-extra.opam
+++ b/coq-itree-extra.opam
@@ -13,7 +13,6 @@ bug-reports: "https://github.com/DeepSpec/InteractionTrees/issues"
 depends: [
   "dune" {>= "3.14"}
   "coq"
-  "coq-ext-lib"
   "coq-paco"
   "coq-itree"
   "odoc" {with-doc}
diff --git a/coq-itree.opam b/coq-itree.opam
index bd48c370..6fa400f9 100644
--- a/coq-itree.opam
+++ b/coq-itree.opam
@@ -20,7 +20,6 @@ bug-reports: "https://github.com/DeepSpec/InteractionTrees/issues"
 depends: [
   "dune" {>= "3.14"}
   "coq" {>= "8.13"}
-  "coq-ext-lib" {>= "0.11.1"}
   "coq-paco" {>= "4.0.1"}
   "odoc" {with-doc}
 ]
diff --git a/dune-project b/dune-project
index d005dfec..791034ee 100644
--- a/dune-project
+++ b/dune-project
@@ -11,7 +11,6 @@
   (synopsis "Library for representing recursive and impure programs with equational reasoning")
   (depends
     (coq (>= 8.13))
-    (coq-ext-lib (>= 0.11.1))
     (coq-paco (>= 4.0.1)))
   (tags ("org:deepspec"))
   (authors
@@ -29,7 +28,6 @@
   (synopsis "Extensions to coq-itree")
   (depends
     coq
-    coq-ext-lib
     coq-paco
     coq-itree)
   (tags ("org:deepspec"))
diff --git a/theories/Basics/Basics.v b/theories/Basics/Basics.v
index c25cbca0..b915e866 100644
--- a/theories/Basics/Basics.v
+++ b/theories/Basics/Basics.v
@@ -3,26 +3,16 @@
 (** Not specific to itrees. *)
 
 (* begin hide *)
-From Coq Require
-     Ensembles.
-
 From Coq Require Import
      RelationClasses.
 
-From ExtLib Require Import
-     Structures.Functor
-     Structures.Monad
-     Data.Monads.StateMonad
-     Data.Monads.ReaderMonad
-     Data.Monads.OptionMonad
-     Data.Monads.EitherMonad.
-
-Import
-  FunctorNotation
-  MonadNotation.
-Local Open Scope monad.
+From stdpp Require Export
+  prelude.
+
+Set Primitive Projections.
 (* end hide *)
 
+
 (** ** Parametric functions *)
 
 (** A notation for a certain class of parametric functions.
@@ -45,41 +35,176 @@ Definition idM {E : Type -> Type} : E ~> E := fun _ e => e.
 (** [void] is a shorthand for [Empty_set]. *)
 Notation void := Empty_set.
 
+(* Canonical equivalence relation for a unary type family. *)
+Class Eq1 (M : Type -> Type) : Type :=
+  eq1 : forall A, M A -> M A -> Prop.
+
+Arguments eq1 {M _ _}.
+Declare Scope monad_scope.
+Open Scope monad_scope.
+Infix "≈" := eq1 (at level 70) : monad_scope.
+
+Class App (T : Type → Type) := ap : ∀ {A B}, T (A → B) → T A → T B.
+
+(* Proof that [eq1] is an equivalence relation. *)
+Class Eq1Equivalence (M : Type -> Type) `{Eq1 M} :=
+  eq1_equiv : forall A, Equivalence (eq1 (A := A)).
+
+#[global] Existing Instance eq1_equiv.
+
+(* Monad laws up to [M]'s canonical equivalence relation. *)
+Class MonadLawsE (M : Type -> Type) `{@Eq1 M, MRet M, MBind M} : Prop :=
+  { bind_ret_l : forall A B (f : A -> M B) (x : A), mret x ≫= f ≈ f x
+  ; bind_ret_r : forall A (x : M A), x ≫= (fun y => mret y) ≈ x
+  ; bind_bind : forall A B C (x : M A) (f : A -> M B) (g : B -> M C),
+      (x ≫= f) ≫= g ≈ x ≫= (fun y => f y ≫= g)
+  ; Proper_bind : forall {A B},
+      (@Proper ((A -> M B) -> M A -> M B)
+         (pointwise_relation _ eq1 ==> eq1 ==> eq1)
+         mbind)
+  }.
+
+#[global] Existing Instance Proper_bind.
+
+Arguments bind_ret_l {M _ _ _ _}.
+Arguments bind_ret_r {M _ _ _ _}.
+Arguments bind_bind {M _ _ _ _}.
+Arguments Proper_bind {M _ _ _ _}.
 (** ** Common monads and transformers. *)
 
-Module Monads.
+Section Monads.
 
+(* id *)
 Definition identity (a : Type) : Type := a.
 
+#[global] Instance FMap_identity : FMap identity
+  := fun _ _ f => f.
+
+#[global] Instance MRet_identity : MRet identity
+  := fun _ a => a.
+
+#[global] Instance MBind_identity : MBind identity
+  := fun _ _ k c => k c.
+
+(* either *)
+Definition either (e a : Type) : Type := sum e a.
+
+#[global] Instance FMap_either {e} : FMap (either e)
+  := fun _ _ f ea => match ea with | inl e => inl e | inr a => inr (f a) end.
+
+#[global] Instance MRet_either {e} : MRet (either e)
+  := fun _ a => inr a.
+
+#[global] Instance MBind_either {e} : MBind (either e)
+  := fun _ _ k c => match c with | inl e => inl e | inr a => k a end.
+
+(* state *)
+Definition state (s a : Type) := s -> prod s a.
+
+#[global] Instance FMap_state {s} : FMap (state s)
+  :=  fun _ _ f run s => (fun sa => (fst sa, f (snd sa))) (run s).
+
+#[global] Instance MRet_state {s} : MRet (state s)
+  := fun _ a s => (s, a).
+
+#[global] Instance MBind_state {s} : MBind (state s) :=
+  fun _ _ k c => fun s => let sa := c s in
+                    k (snd sa) (fst sa).
+
+(* reader *)
+Definition reader (r a : Type) := r -> a.
+
+#[global] Instance FMap_reader {r} : FMap (reader r)
+  :=  fun _ _ f run r => f (run r).
+
+#[global] Instance MRet_reader {r} : MRet (reader r)
+  := fun _ a _ => a.
+
+#[global] Instance MBind_reader {r} : MBind (reader r) :=
+  fun _ _ k c => fun r => k (c r) r.
+
+(* writer *)
+Definition writer := prod.
+
+(* optionT *)
+
+Definition optionT (m : Type -> Type) (a : Type) : Type :=
+  m (option a).
+
+#[global] Instance FMap_optionT {m} {Fm : FMap m} : FMap (optionT m)
+  := fun _ _ f c => (fun x => match x with | None => None | Some x => Some (f x) end ) <$> c.
+
+#[global] Instance MRet_optionT {m} {Fm : MRet m} : MRet (optionT m)
+  := fun _ a => mret (Some a).
+
+#[global] Instance MBind_optionT {m} `{MRet m, MBind m} : MBind (optionT m) :=
+  fun _ _ k c => mbind (M := m) (fun oa => match oa with
+                                     | None   => mret (M := m) None
+                                     | Some a => k a
+                                     end) c.
+
+Definition run_optionT {m a} (x : optionT m a) : m (option a)%type := x.
+
+Definition liftOption {a f} `{FMap f} (fa : f a) : optionT f a :=
+  Some <$> fa.
+
+(* eitherT *)
+Definition eitherT (e : Type) (m : Type -> Type) (a : Type) : Type := m (sum e a).
+
+#[global] Instance FMap_eitherT {e m} `{FMap m} : FMap (eitherT e m)
+  := fun _ _ f c => (fun ea => match ea with | inl e => inl e | inr a => inr (f a) end) <$> c.
+
+#[global] Instance MRet_eitherT {e m} `{MRet m} : MRet (eitherT e m)
+  := fun _ a => mret (inr a).
+
+#[global] Instance MBind_eitherT {e m} `{MRet m, MBind m} : MBind (eitherT e m)
+  := fun _ _ f => mbind (M := m) (fun ea => match ea with | inl e => mret (inl e) | inr a => f a end).
+
+Definition runEither {e m a} (x : eitherT e m a) : m (sum e a) := x.
+
+Definition liftEither {e f a} `{FMap f} (fa : f a) : eitherT e f a := inr <$> fa.
+
+(* stateT *)
 Definition stateT (s : Type) (m : Type -> Type) (a : Type) : Type :=
   s -> m (prod s a).
-Definition state (s a : Type) := s -> prod s a.
+
+#[global] Instance FMap_stateT {m s} {Fm : FMap m} : FMap (stateT s m)
+  :=  fun _ _ f run s => fmap (fun sa => (fst sa, f (snd sa))) (run s).
+
+#[global] Instance MRet_stateT {m s} {Fm : MRet m} : MRet (stateT s m)
+  := fun _ a s => mret (s, a).
+
+#[global] Instance MBind_stateT {m s} {Fm : MBind m} : MBind (stateT s m) :=
+  fun _ _ k c => fun s => sa ← c s ;
+                    k (snd sa) (fst sa).
 
 Definition run_stateT {s m a} (x : stateT s m a) : s -> m (s * a)%type := x.
 
-Definition liftState {s a f} `{Functor f} (fa : f a) : Monads.stateT s f a :=
+Definition liftState {s a f} `{FMap f} (fa : f a) : stateT s f a :=
   fun s => pair s <$> fa.
 
+(* readerT *)
 Definition readerT (r : Type) (m : Type -> Type) (a : Type) : Type :=
   r -> m a.
-Definition reader (r a : Type) := r -> a.
 
-Definition writerT (w : Type) (m : Type -> Type) (a : Type) : Type :=
-  m (prod w a).
-Definition writer := prod.
+#[global] Instance FMap_readerT {m r} {Fm : FMap m} : FMap (readerT r m)
+  :=  fun _ _ f run r => fmap f (run r).
 
-#[global] Instance Functor_stateT {m s} {Fm : Functor m} : Functor (stateT s m)
-  := {|
-    fmap _ _ f := fun run s => fmap (fun sa => (fst sa, f (snd sa))) (run s)
-    |}.
+#[global] Instance MRet_readerT {m r} {Fm : MRet m} : MRet (readerT r m)
+  := fun _ a _ => mret a.
 
-#[global] Instance Monad_stateT {m s} {Fm : Monad m} : Monad (stateT s m)
-  := {|
-    ret _ a := fun s => ret (s, a)
-  ; bind _ _ t k := fun s =>
-      sa <- t s ;;
-      k (snd sa) (fst sa)
-    |}.
+#[global] Instance MBind_readerT {m r} {Fm : MBind m} : MBind (readerT r m) :=
+  fun _ _ k c => fun r => v ← c r ;
+                    k v r.
+
+Definition run_readerT {r m a} (x : readerT r m a) : r -> m a%type := x.
+
+Definition liftReader {r a f} `{FMap f} (fa : f a) : readerT r f a :=
+  fun _ => fa.
+
+(* writerT *)
+Definition writerT (w : Type) (m : Type -> Type) (a : Type) : Type :=
+  m (prod w a).
 
 End Monads.
 
@@ -101,71 +226,62 @@ Polymorphic Class MonadIter (M : Type -> Type) : Type :=
     Quite easily in fact, no [Monad] assumption needed.
  *)
 
-#[global] Instance MonadIter_stateT {M S} {MM : Monad M} {AM : MonadIter M}
+#[global] Polymorphic Instance MonadIter_stateT {M S} `{MRet M, MBind M, MonadIter M}
   : MonadIter (stateT S M) :=
-  fun _ _ step i => mkStateT (fun s =>
-    iter (fun is =>
-      let i := fst is in
-      let s := snd is in
-      is' <- runStateT (step i) s ;;
-      ret match fst is' with
-          | inl i' => inl (i', snd is')
-          | inr r => inr (r, snd is')
-          end) (i, s)).
-
-#[global] Polymorphic Instance MonadIter_stateT0 {M S} {MM : Monad M} {AM : MonadIter M}
-  : MonadIter (Monads.stateT S M) :=
   fun _ _ step i s =>
     iter (fun si =>
-      let s := fst si in
-      let i := snd si in
-      si' <- step i s;;
-      ret match snd si' with
-          | inl i' => inl (fst si', i')
-          | inr r => inr (fst si', r)
-          end) (s, i).
+            let s := fst si in
+            let i := snd si in
+            si' ← step i s;
+            mret match snd si' with
+              | inl i' => inl (fst si', i')
+              | inr r => inr (fst si', r)
+              end) (s, i).
 
 #[global] Instance MonadIter_readerT {M S} {AM : MonadIter M} : MonadIter (readerT S M) :=
-  fun _ _ step i => mkReaderT (fun s =>
-    iter (fun i => runReaderT (step i) s) i).
+  fun _ _ step i => fun r =>
+    iter (fun i => run_readerT (step i) r) i.
 
-#[global] Instance MonadIter_optionT {M} {MM : Monad M} {AM : MonadIter M}
+#[global] Instance MonadIter_optionT {M} `{MRet M, MBind M, MonadIter M}
   : MonadIter (optionT M) :=
-  fun _ _ step i => mkOptionT (
+  fun _ _ step i =>
     iter (fun i =>
-      oi <- unOptionT (step i) ;;
-      ret match oi with
-          | None => inr None
-          | Some (inl i) => inl i
-          | Some (inr r) => inr (Some r)
-          end) i).
-
-#[global] Instance MonadIter_eitherT {M E} {MM : Monad M} {AM : MonadIter M}
+            oi ← step i ;
+            mret match oi with
+              | None => inr None
+              | Some (inl i) => inl i
+              | Some (inr r) => inr (Some r)
+              end) i.
+
+#[global] Instance MonadIter_eitherT {M E} `{MRet M, MBind M, MonadIter M} {AM : MonadIter M}
   : MonadIter (eitherT E M) :=
-  fun _ _ step i => mkEitherT (
+  fun _ _ step i =>
     iter (fun i =>
-      ei <- unEitherT (step i) ;;
-      ret match ei with
-          | inl e => inr (inl e)
-          | inr (inl i) => inl i
-          | inr (inr r) => inr (inr r)
-          end) i).
+            ei ← step i ;
+            mret match ei with
+              | inl e => inr (inl e)
+              | inr (inl i) => inl i
+              | inr (inr r) => inr (inr r)
+              end) i.
 
 (** And the nondeterminism monad [_ -> Prop] also has one. *)
+From stdpp Require Import propset.
 
-Inductive iter_Prop {R I : Type} (step : I -> I + R -> Prop) (i : I) (r : R)
+Inductive iter_Prop {R I : Type} (step : I -> propset (I + R)) (i : I) (r : R)
   : Prop :=
 | iter_done
-  : step i (inr r) -> iter_Prop step i r
+  : propset_car (step i) (inr r) -> iter_Prop step i r
 | iter_step i'
-  : step i (inl i') ->
+  : propset_car (step i) (inl i') ->
     iter_Prop step i' r ->
     iter_Prop step i r
 .
 
-#[global] Polymorphic Instance MonadIter_Prop : MonadIter Ensembles.Ensemble := @iter_Prop.
+#[global] Polymorphic Instance MonadIter_Prop : MonadIter propset :=
+  fun _ _ step i => PropSet (iter_Prop step i).
 
 (* Elementary constructs for predicates. To be moved in their own file eventually *)
+(* TODO: should they be entirely replaced with constructions in [propset]? *)
 Definition equiv_pred {A : Type} (R S: A -> Prop): Prop :=
   forall a, R a <-> S a.
 
@@ -194,4 +310,3 @@ Qed.
 Proof.
   split; typeclasses eauto.
 Qed.
-
diff --git a/theories/Basics/CategoryKleisli.v b/theories/Basics/CategoryKleisli.v
index 6b8127c8..45f80fc1 100644
--- a/theories/Basics/CategoryKleisli.v
+++ b/theories/Basics/CategoryKleisli.v
@@ -18,14 +18,10 @@
 From Coq Require Import
      Morphisms.
 
-From ExtLib Require Import
-     Structures.Monad.
-
 From ITree Require Import
      Basics.Basics
      Basics.CategoryOps
-     Basics.Function
-     Basics.Monad.
+     Basics.Function.
 (* end hide *)
 
 Implicit Types m : Type -> Type.
@@ -39,12 +35,12 @@ Definition Kleisli_arrow {m a b} : (a -> m b) -> Kleisli m a b := fun f => f.
 Definition Kleisli_apply {m a b} : Kleisli m a b -> (a -> m b) := fun f => f.
 
 
-Definition pure {m} `{Monad m} {a b} (f : a -> b) : Kleisli m a b :=
-  fun x => ret (f x).
+Definition pure {m} `{MRet m} {a b} (f : a -> b) : Kleisli m a b :=
+  fun x => mret (f x).
 
 Section Instances.
   Context {m : Type -> Type}.
-  Context `{Monad m}.
+  Context `{MRet m, MBind m}.
   Context `{Eq1 m}.
 
   #[global] Instance Eq2_Kleisli : Eq2 (Kleisli m) :=
@@ -52,11 +48,11 @@ Section Instances.
 
   #[global] Instance Cat_Kleisli : Cat (Kleisli m) :=
     fun _ _ _ u v x =>
-      bind (u x) (fun y => v y).
+      u x ≫= (fun y => v y).
 
   Definition map {a b c} (g:b -> c) (ab : Kleisli m a b) : Kleisli m a c :=
      cat ab (pure g).
-  
+
   #[global] Instance Initial_Kleisli : Initial (Kleisli m) void :=
     fun _ v => match v : void with end.
 
diff --git a/theories/Basics/CategoryKleisliFacts.v b/theories/Basics/CategoryKleisliFacts.v
index dbd582ad..6ac1e66b 100644
--- a/theories/Basics/CategoryKleisliFacts.v
+++ b/theories/Basics/CategoryKleisliFacts.v
@@ -6,13 +6,9 @@ From Coq Require Import
      Morphisms
      RelationClasses.
 
-From ExtLib Require Import
-     Structures.Monad.
-
 From ITree Require Import
      Basics.Basics
      Basics.Category
-     Basics.Monad
      Basics.CategoryFunctor
      Basics.CategoryKleisli
      Basics.Function.
@@ -26,10 +22,11 @@ Section BasicFacts.
 
   Context {m : Type -> Type}.
   Context {Eq1 : Eq1 m}.
-  Context {Mm : Monad m}.
-  Context {Eq1P : @Eq1Equivalence m _ Eq1}.
-  Context {ML : @MonadLawsE m Eq1 Mm}.
-  
+  Context {Mr : MRet m}.
+  Context {Mb : MBind m}.
+  Context {Eq1P : @Eq1Equivalence m Eq1}.
+  Context {ML : @MonadLawsE m Eq1 Mr Mb}.
+
   Instance Proper_Kleisli_apply {a b} :
     Proper (eq2 ==> eq ==> eq1) (@Kleisli_apply m a b).
   Proof.
@@ -38,8 +35,8 @@ Section BasicFacts.
 
   Lemma fold_Kleisli {a b} (f : Kleisli m a b) (x : a) : f x = Kleisli_apply f x.
   Proof. reflexivity. Qed.
-  
-  Global Instance Equivalence_Kleisli_eq2 {a b} : @Equivalence (Kleisli m a b) eq2.
+
+  #[global] Instance Equivalence_Kleisli_eq2 {a b} : @Equivalence (Kleisli m a b) eq2.
   Proof.
     split; repeat intro.
     - reflexivity.
@@ -47,7 +44,7 @@ Section BasicFacts.
     - etransitivity; eauto.
   Qed.
 
-  Global Instance Functor_pure
+  #[global] Instance Functor_pure
     : Functor Fun (Kleisli m) (fun x => x) (@pure m _).
   Proof.
     constructor; intros.
@@ -57,277 +54,275 @@ Section BasicFacts.
     - intros ? ? ? ?. unfold pure. rewrite H. reflexivity.
   Qed.
 
-(* This is subsumed by [category_proper_cat] and the [Category]
+  (* This is subsumed by [category_proper_cat] and the [Category]
    instance for Kleisli.
-   Adding this as an instance (i.e., marking this as [Global]) would confuse
+   Adding this as an instance (i.e., marking this as [#[global]]) would confuse
    typeclass search, as it would often be picked for categories whose arrow
    types are definitionally equal to some [Kleisli m a b]
    (e.g., [sub (Kleisli m) f]), which puts the rest of the search in the wrong
    category.
- *)
-Instance Proper_cat_Kleisli {a b c}
-  : @Proper (Kleisli m a b -> Kleisli m b c -> _)
-            (eq2 ==> eq2 ==> eq2) cat.
-Proof.
-  repeat intro.
-  unfold cat, Cat_Kleisli.
-  apply Proper_bind; auto.
-Qed.
-
-Local Opaque bind ret eq1.
-
-Lemma pure_assoc_l {a b c : Type}
-  : assoc_l (C := Kleisli m) (bif := sum)
-  ⩯ pure (m := m) (a := a + (b + c))%type assoc_l.
-Proof.
-  cbv; intros x; destruct x as [ | []]; try setoid_rewrite bind_ret_l; reflexivity.
-Qed.
-
-Lemma pure_assoc_r {a b c : Type} :
-  (@assoc_r _ (Kleisli m) sum _ _ _ _) ⩯ (@pure m _ ((a + b) + c)%type _ assoc_r).
-Proof.
-  cbv; intros x; destruct x as [[] | ]; try setoid_rewrite bind_ret_l; reflexivity.
-Qed.
-
-Global Instance CatAssoc_Kleisli : CatAssoc (Kleisli m).
-Proof.
-  red. intros a b c d f g h. 
-  unfold cat, Cat_Kleisli.
-  cbv. intros x.
-  setoid_rewrite bind_bind.
-  reflexivity.
-Qed.
-
-(** *** [id_ktree] respect identity laws *)
-Global Instance CatIdL_Kleisli : CatIdL (Kleisli m).
-Proof.
-  intros A B f a; unfold cat, Cat_Kleisli, id_, Id_Kleisli, pure.
-  rewrite bind_ret_l. reflexivity.
-Qed.
-
-Global Instance CatIdR_Kleisli : CatIdR (Kleisli m).
-Proof.
-  intros A B f a; unfold cat, Cat_Kleisli, id_, Id_Kleisli, pure.
-  rewrite bind_ret_r.
-  reflexivity.
-Qed.
-
-Global Instance Category_Kleisli : Category (Kleisli m).
-Proof.
-  constructor; typeclasses eauto.
-Qed.
-
-Global Instance InitialObject_Kleisli : InitialObject (Kleisli m) void.
-Proof. intros A f []. Qed.
-
-
-
-Global Instance Proper_case_Kleisli {a b c}
-  : @Proper (Kleisli m a c -> Kleisli m b c -> _)
-            (eq2 ==> eq2 ==> eq2) case_.
-Proof.
-  repeat intro; destruct (_ : _ + _); cbn; auto.
-Qed.
-
-(** *** [pure] is well-behaved *)
-
-(* SAZ: not sure about the naming conventions here. *)
-
-Global Instance Proper_pure {A B} :
-  Proper (eq2 ==> eq2) (@pure _ _ A B).
-Proof.
-  repeat intro.
-  unfold pure.
-  erewrite (H a); reflexivity.
-Qed.
-
-Lemma pure_id {A: Type}: (id_ A ⩯ @pure _ _ A A (id_ A))%cat.
-Proof.
-  reflexivity.
-Qed.
-
-Fact compose_pure {A B C} (ab : A -> B) (bc : B -> C) :
-  (pure ab >>> pure bc ⩯ pure (ab >>> bc))%cat.
-Proof.
-  intros a.
-  unfold pure, cat, Cat_Kleisli.
-  rewrite bind_ret_l.
-  reflexivity.
-Qed.
-
-Fact compose_pure_l {A B C D} (f: A -> B) (g: B -> C) (k: Kleisli m C D) :
-  (pure f >>> (pure g >>> k) ⩯ pure (g ∘ f) >>> k)%cat.
-Proof.
-  rewrite <- cat_assoc.
-  rewrite compose_pure.
-  reflexivity.
-Qed.
-
-Fact compose_pure_r {A B C D} (f: B -> C) (g: C -> D) (k: Kleisli m A B) :
-  ((k >>> pure f) >>> pure g ⩯ k >>> pure (g ∘ f))%cat.
-Proof.
-  rewrite cat_assoc.
-  rewrite compose_pure.
-  reflexivity.
-Qed.
-
-Fact pure_cat {A B C}: forall (f:A -> B) (bc: Kleisli m B C),
-    pure f >>> bc ⩯ fun a => bc (f a).
-Proof.
-  intros; intro a.
-  unfold pure, pure, cat, Cat_Kleisli.
-  rewrite bind_ret_l. reflexivity.
-Qed.
-
-
-Fact cat_pure {A B C}: forall (ab: Kleisli m A B) (g:B -> C),
-    (ab >>> pure g)
-  ⩯ (map g ab).
-Proof.
-  reflexivity.
-Qed.
-
-Lemma pure_swap {A B}:
-  @pure _ _ (A+B) _ swap ⩯ swap.
-Proof.
-  intros []; reflexivity.
-Qed.
-
-Lemma pure_inl {A B}
-  : pure (b := A + B) inl_ ⩯ inl_.
-Proof. reflexivity. Qed.
-
-Lemma pure_inr {A B}
-  : pure (b := A + B) inr_ ⩯ inr_.
-Proof. reflexivity. Qed.
-
-Lemma case_pure {A B C} (ac : A -> C) (bc : B -> C) :
+   *)
+  Instance Proper_cat_Kleisli {a b c}
+    : @Proper (Kleisli m a b -> Kleisli m b c -> _)
+        (eq2 ==> eq2 ==> eq2) cat.
+  Proof.
+    repeat intro.
+    unfold cat, Cat_Kleisli.
+    apply Proper_bind; auto.
+  Qed.
+
+  (* Local Opaque bind ret eq1. *)
+
+  Lemma pure_assoc_l {a b c : Type}
+    : assoc_l (C := Kleisli m) (bif := sum)
+        ⩯ pure (m := m) (a := a + (b + c))%type assoc_l.
+  Proof.
+    cbv; intros x; destruct x as [ | []]; try setoid_rewrite bind_ret_l; reflexivity.
+  Qed.
+
+  Lemma pure_assoc_r {a b c : Type} :
+    (@assoc_r _ (Kleisli m) sum _ _ _ _) ⩯ (@pure m _ ((a + b) + c)%type _ assoc_r).
+  Proof.
+    cbv; intros x; destruct x as [[] | ]; try setoid_rewrite bind_ret_l; reflexivity.
+  Qed.
+
+  #[global] Instance CatAssoc_Kleisli : CatAssoc (Kleisli m).
+  Proof.
+    red. intros a b c d f g h.
+    unfold cat, Cat_Kleisli.
+    cbv. intros x.
+    setoid_rewrite bind_bind.
+    reflexivity.
+  Qed.
+
+  (** *** [id_ktree] respect identity laws *)
+  #[global] Instance CatIdL_Kleisli : CatIdL (Kleisli m).
+  Proof.
+    intros A B f a; unfold cat, Cat_Kleisli, id_, Id_Kleisli, pure.
+    rewrite bind_ret_l. reflexivity.
+  Qed.
+
+  #[global] Instance CatIdR_Kleisli : CatIdR (Kleisli m).
+  Proof.
+    intros A B f a; unfold cat, Cat_Kleisli, id_, Id_Kleisli, pure.
+    rewrite bind_ret_r.
+    reflexivity.
+  Qed.
+
+  #[global] Instance Category_Kleisli : Category (Kleisli m).
+  Proof.
+    constructor; typeclasses eauto.
+  Qed.
+
+  #[global] Instance InitialObject_Kleisli : InitialObject (Kleisli m) void.
+  Proof. intros A f []. Qed.
+
+  #[global] Instance Proper_case_Kleisli {a b c}
+    : @Proper (Kleisli m a c -> Kleisli m b c -> _)
+        (eq2 ==> eq2 ==> eq2) case_.
+  Proof.
+    repeat intro; destruct (_ : _ + _); cbn; auto.
+  Qed.
+
+  (** *** [pure] is well-behaved *)
+
+  (* SAZ: not sure about the naming conventions here. *)
+
+  #[global] Instance Proper_pure {A B} :
+    Proper (eq2 ==> eq2) (@pure _ _ A B).
+  Proof.
+    repeat intro.
+    unfold pure.
+    erewrite (H a); reflexivity.
+  Qed.
+
+  Lemma pure_id {A: Type}: (id_ (C := Kleisli m) A ⩯ @pure _ _ A A (id_ A))%cat.
+  Proof.
+    reflexivity.
+  Qed.
+
+  Fact compose_pure {A B C} (ab : A -> B) (bc : B -> C) :
+    (pure (m := m) ab >>> pure bc ⩯ pure (ab >>> bc))%cat.
+  Proof.
+    intros a.
+    unfold pure, cat, Cat_Kleisli.
+    rewrite bind_ret_l.
+    reflexivity.
+  Qed.
+
+  Fact compose_pure_l {A B C D} (f: A -> B) (g: B -> C) (k: Kleisli m C D) :
+    (pure f >>> (pure g >>> k) ⩯ pure (g ∘ f) >>> k)%cat.
+  Proof.
+    rewrite <- cat_assoc.
+    rewrite compose_pure.
+    reflexivity.
+  Qed.
+
+  Fact compose_pure_r {A B C D} (f: B -> C) (g: C -> D) (k: Kleisli m A B) :
+    ((k >>> pure f) >>> pure g ⩯ k >>> pure (g ∘ f))%cat.
+  Proof.
+    rewrite cat_assoc.
+    rewrite compose_pure.
+    reflexivity.
+  Qed.
+
+  Fact pure_cat {A B C}: forall (f:A -> B) (bc: Kleisli m B C),
+      pure f >>> bc ⩯ fun a => bc (f a).
+  Proof.
+    intros; intro a.
+    unfold pure, pure, cat, Cat_Kleisli.
+    rewrite bind_ret_l. reflexivity.
+  Qed.
+
+
+  Fact cat_pure {A B C}: forall (ab: Kleisli m A B) (g:B -> C),
+      (ab >>> pure g)
+        ⩯ (map g ab).
+  Proof.
+    reflexivity.
+  Qed.
+
+  Lemma pure_swap {A B}:
+    @pure _ _ (A+B) _ swap ⩯ swap.
+  Proof.
+    intros []; reflexivity.
+  Qed.
+
+  Lemma pure_inl {A B}
+    : pure (m := m) (b := A + B) inl_ ⩯ inl_.
+  Proof. reflexivity. Qed.
+
+  Lemma pure_inr {A B}
+    : pure (m := m) (b := A + B) inr_ ⩯ inr_.
+  Proof. reflexivity. Qed.
+
+  Lemma case_pure {A B C} (ac : A -> C) (bc : B -> C) :
     case_ (pure ac) (pure bc)
-  ⩯ pure (@case_ _ Fun _ _ _ _ _ ac bc).
-Proof.
-  intros []; reflexivity.
-Qed.
-
-(** *** [Unitors] lemmas *)
-
-(* This is probably generalizable into [Basics.Category]. *)
-
-Lemma unit_l_pure (A : Type) :
-  unit_l ⩯ @pure _ _ (void + A) A unit_l.
-Proof.
-  intros [[]|]. reflexivity.
-Qed.
-
-Lemma unit_l'_pure (A : Type) :
-  unit_l' ⩯ @pure _ _ A (void + A) unit_l'.
-Proof.
-  reflexivity.
-Qed.
-
-Lemma unit_r_pure (A : Type) :
-  unit_r ⩯ @pure _ _ (A + void) A unit_r.
-Proof.
-  intros [|[]]. reflexivity.
-Qed.
-
-Lemma unit_r'_pure (A : Type) :
-  unit_r' ⩯ @pure _ _ A (A + void) unit_r'.
-Proof.
-  reflexivity.
-Qed.
-
-(* SAZ: was named "case_l_ktree" *)
-Lemma case_l {A B: Type} (ab: Kleisli m A (void + B)) :
-  ab >>> unit_l ⩯ map unit_l ab.
-Proof.
-  rewrite unit_l_pure.
-  reflexivity.
-Qed.
-
-(* SAZ: was named "case_l'_ktree" *)
-Lemma case_l' {A B: Type} (f: Kleisli m (void + A) (void + B)) :
-  unit_l' >>> f ⩯ fun a => f (inr a).
-Proof.
-  rewrite unit_l'_pure.
-  intro. unfold cat, Cat_Kleisli, pure.
-  rewrite bind_ret_l; reflexivity.
-Qed.
-
-
-Lemma case_r {A B: Type} (ab: Kleisli m A (B + void)) :
-  ab >>> unit_r ⩯ map unit_r ab.
-Proof.
-  rewrite unit_r_pure.
-  reflexivity.
-Qed.
-
-Lemma case_r' {A B: Type} (f: Kleisli m (A + void) (B + void)) :
-  unit_r' >>> f ⩯ fun a => f (inl a).
-Proof.
-  rewrite unit_r'_pure.
-  intro. unfold cat, Cat_Kleisli, pure.
-  rewrite bind_ret_l; reflexivity.
-Qed.
-
-
-Fact bimap_id_pure {A B C} (f : B -> C) :
-  bimap (id_ A) (pure f) ⩯ pure (bimap (id_ A) f).
-Proof.
-  unfold bimap, Bimap_Coproduct.
-  rewrite !cat_id_l. rewrite <- !case_pure. rewrite <- !compose_pure. rewrite <- pure_id.
-  rewrite !cat_id_l. 
-  reflexivity.
-Qed.
-
-Fact bimap_pure_id {A B C} (f : A -> B) :
-  bimap (pure f) (id_ C) ⩯ pure (bimap f id).
-Proof.
-  unfold bimap, Bimap_Coproduct.
-  rewrite !cat_id_l, <- case_pure, <- compose_pure.
-  reflexivity.
-Qed.
-
-Global Instance Coproduct_Kleisli : Coproduct (Kleisli m) sum.
-Proof.
-  constructor.
-  - intros a b c f g.
-    unfold inl_, Inl_Kleisli.
-    rewrite pure_cat.
+      ⩯ pure (m := m) (@case_ _ Fun _ _ _ _ _ ac bc).
+  Proof.
+    intros []; reflexivity.
+  Qed.
+
+  (** *** [Unitors] lemmas *)
+
+  (* This is probably generalizable into [Basics.Category]. *)
+
+  Lemma unit_l_pure (A : Type) :
+    unit_l ⩯ @pure m _ (void + A) A unit_l.
+  Proof.
+    intros [[]|]. reflexivity.
+  Qed.
+
+  Lemma unit_l'_pure (A : Type) :
+    unit_l' ⩯ @pure m _ A (void + A) unit_l'.
+  Proof.
+    reflexivity.
+  Qed.
+
+  Lemma unit_r_pure (A : Type) :
+    unit_r ⩯ @pure m _ (A + void) A unit_r.
+  Proof.
+    intros [|[]]. reflexivity.
+  Qed.
+
+  Lemma unit_r'_pure (A : Type) :
+    unit_r' ⩯ @pure m _ A (A + void) unit_r'.
+  Proof.
     reflexivity.
-  - intros a b c f g.
-    unfold inr_, Inr_Kleisli.
-    rewrite pure_cat.
+  Qed.
+
+  (* SAZ: was named "case_l_ktree" *)
+  Lemma case_l {A B: Type} (ab: Kleisli m A (void + B)) :
+    ab >>> unit_l ⩯ map unit_l ab.
+  Proof.
+    rewrite unit_l_pure.
     reflexivity.
-  - intros a b c f g fg Hf Hg [x | y].
-    + unfold inl_, Inl_Kleisli in Hf.
-      rewrite pure_cat in Hf.
-      specialize (Hf x). simpl in Hf. rewrite Hf. reflexivity.
-    + unfold inr_, Inr_Kleisli in Hg.
-      rewrite pure_cat in Hg.
-      specialize (Hg y). simpl in Hg. rewrite Hg. reflexivity.
-  - typeclasses eauto.
-Qed.
-
-Global Instance bimap_id_kleisli : BimapId (Kleisli m) sum.
-Proof.
-  unfold BimapId, bimap, Bimap_Coproduct.
-  intros.
-  rewrite! cat_id_l.
-  unfold inl_, inr_, Inl_Kleisli, Inr_Kleisli.
-  rewrite case_pure.
-  unfold pure, id_, case_, Case_Kleisli, case_sum, Id_Kleisli, pure.
-  red. intro. destruct a0; reflexivity.
-Qed.  
+  Qed.
+
+  (* SAZ: was named "case_l'_ktree" *)
+  Lemma case_l' {A B: Type} (f: Kleisli m (void + A) (void + B)) :
+    unit_l' >>> f ⩯ fun a => f (inr a).
+  Proof.
+    rewrite unit_l'_pure.
+    intro. unfold cat, Cat_Kleisli, pure.
+    rewrite bind_ret_l; reflexivity.
+  Qed.
+
+  Lemma case_r {A B: Type} (ab: Kleisli m A (B + void)) :
+    ab >>> unit_r ⩯ map unit_r ab.
+  Proof.
+    rewrite unit_r_pure.
+    reflexivity.
+  Qed.
+
+  Lemma case_r' {A B: Type} (f: Kleisli m (A + void) (B + void)) :
+    unit_r' >>> f ⩯ fun a => f (inl a).
+  Proof.
+    rewrite unit_r'_pure.
+    intro. unfold cat, Cat_Kleisli, pure.
+    rewrite bind_ret_l; reflexivity.
+  Qed.
+
+
+  Fact bimap_id_pure {A B C} (f : B -> C) :
+    bimap (id_ A) (pure f) ⩯ pure (m := m) (bimap (id_ A) f).
+  Proof.
+    unfold bimap, Bimap_Coproduct.
+    rewrite !cat_id_l. rewrite <- !case_pure. rewrite <- !compose_pure. rewrite <- pure_id.
+    rewrite !cat_id_l.
+    reflexivity.
+  Qed.
+
+  Fact bimap_pure_id {A B C} (f : A -> B) :
+    bimap (pure f) (id_ C) ⩯ pure (m := m) (bimap f id).
+  Proof.
+    unfold bimap, Bimap_Coproduct.
+    rewrite !cat_id_l, <- case_pure, <- compose_pure.
+    reflexivity.
+  Qed.
+
+  #[global] Instance Coproduct_Kleisli : Coproduct (Kleisli m) sum.
+  Proof.
+    constructor.
+    - intros a b c f g.
+      unfold inl_, Inl_Kleisli.
+      rewrite pure_cat.
+      reflexivity.
+    - intros a b c f g.
+      unfold inr_, Inr_Kleisli.
+      rewrite pure_cat.
+      reflexivity.
+    - intros a b c f g fg Hf Hg [x | y].
+      + unfold inl_, Inl_Kleisli in Hf.
+        rewrite pure_cat in Hf.
+        specialize (Hf x). simpl in Hf. rewrite Hf. reflexivity.
+      + unfold inr_, Inr_Kleisli in Hg.
+        rewrite pure_cat in Hg.
+        specialize (Hg y). simpl in Hg. rewrite Hg. reflexivity.
+    - typeclasses eauto.
+  Qed.
+
+  #[global] Instance bimap_id_kleisli : BimapId (Kleisli m) sum.
+  Proof.
+    unfold BimapId, bimap, Bimap_Coproduct.
+    intros.
+    rewrite! cat_id_l.
+    unfold inl_, inr_, Inl_Kleisli, Inr_Kleisli.
+    rewrite case_pure.
+    unfold pure, id_, case_, Case_Kleisli, case_sum, Id_Kleisli, pure.
+    red. intro. destruct a0; reflexivity.
+  Qed.
 
   Lemma map_inl_case_kleisli:
     forall (a1 b1 b2 c1 c2 : Type) (f1 : Kleisli m a1 b1) (g1 : Kleisli m b1 c1) (g2 : Kleisli m b2 c2),
-      map inl f1 >>> case_ (map inl g1) (map inr g2) ⩯ map inl (f1 >>> g1).
+      map (m := m) inl f1 >>> case_ (map inl g1) (map inr g2) ⩯ map inl (f1 >>> g1).
   Proof.
     intros a1 b1 b2 c1 c2 f1 g1 g2.
     unfold cat, Cat_Kleisli, case_, Case_Kleisli, case_sum.
     unfold map. unfold cat, Cat_Kleisli.
     setoid_rewrite bind_bind.
-    unfold pure. setoid_rewrite bind_ret_l. reflexivity.
+    unfold pure.
+    setoid_rewrite bind_ret_l. reflexivity.
   Qed.
 
   Lemma map_inr_case_kleisli:
@@ -342,32 +337,32 @@ Qed.
   Qed.
 
 
-Global Instance bimap_cat_kleisli : BimapCat (Kleisli m) sum.
-Proof.
-  unfold BimapCat, bimap, Bimap_Coproduct.
-  intros.
-  unfold inl_, inr_, Inl_Kleisli, Inr_Kleisli.
-  rewrite! cat_pure. rewrite! cat_case.
-  rewrite map_inl_case_kleisli.
-  rewrite map_inr_case_kleisli.
-  reflexivity.
-Qed.
-
-Global Instance proper_bimap_kleisli : forall a b c d,
-    @Proper (Kleisli m a c -> Kleisli m b d -> Kleisli m _ _) (eq2 ==> eq2 ==> eq2) bimap.
-Proof.
-  intros.
-  repeat intro.
-  unfold bimap, Bimap_Coproduct.
-  unfold case_, Case_Kleisli, case_sum.
-  destruct a0.
-  - unfold cat, Cat_Kleisli, inl_. rewrite H. reflexivity.
-  - unfold cat, Cat_Kleisli, inl_. rewrite H0. reflexivity.
-Qed.
-
-Global Instance Bifunctor_Kleisli : Bifunctor (Kleisli m) sum.
-constructor; typeclasses eauto.
-Qed.
+  #[global] Instance bimap_cat_kleisli : BimapCat (Kleisli m) sum.
+  Proof.
+    unfold BimapCat, bimap, Bimap_Coproduct.
+    intros.
+    unfold inl_, inr_, Inl_Kleisli, Inr_Kleisli.
+    rewrite! cat_pure. rewrite! cat_case.
+    rewrite map_inl_case_kleisli.
+    rewrite map_inr_case_kleisli.
+    reflexivity.
+  Qed.
+
+  #[global] Instance proper_bimap_kleisli : forall a b c d,
+      @Proper (Kleisli m a c -> Kleisli m b d -> Kleisli m _ _) (eq2 ==> eq2 ==> eq2) bimap.
+  Proof.
+    intros.
+    repeat intro.
+    unfold bimap, Bimap_Coproduct.
+    unfold case_, Case_Kleisli, case_sum.
+    destruct a0.
+    - unfold cat, Cat_Kleisli, inl_. rewrite H. reflexivity.
+    - unfold cat, Cat_Kleisli, inl_. rewrite H0. reflexivity.
+  Qed.
+
+  #[global] Instance Bifunctor_Kleisli : Bifunctor (Kleisli m) sum.
+  constructor; typeclasses eauto.
+  Qed.
 
 End BasicFacts.
 
diff --git a/theories/Basics/Function.v b/theories/Basics/Function.v
index 6fcf82ce..97f93f3c 100644
--- a/theories/Basics/Function.v
+++ b/theories/Basics/Function.v
@@ -64,6 +64,6 @@ Definition apply_Fun {A B : Type} (f : Fun A B) : A -> B := f.
 (** The [exponential] is just [_ -> _], which is a just another name for [Fun] *)
 #[global] Instance Apply_Fun : Apply Fun prod Fun :=
     fun {A B} '(f, b) => f b.
-  
+
 #[global] Instance Curry_Fun : Curry Fun prod Fun :=
   fun {A B C} f => fun c a => f (c, a).
diff --git a/theories/Basics/Monad.v b/theories/Basics/Monad.v
deleted file mode 100644
index 68fc2f0c..00000000
--- a/theories/Basics/Monad.v
+++ /dev/null
@@ -1,59 +0,0 @@
-(** * Monad laws and associated typeclasses *)
-
-(* begin hide *)
-From Coq Require Import
-     Morphisms.
-
-From ExtLib Require Export
-     Structures.Monad.
-
-From ITree Require Import
-     Basics.Basics
-     Basics.CategoryOps.
-(* end hide *)
-
-Set Primitive Projections.
-
-(* Canonical equivalence relation for a unary type family. *)
-Class Eq1 (M : Type -> Type) : Type :=
-  eq1 : forall A, M A -> M A -> Prop.
-
-Arguments eq1 {M _ _}.
-Infix "≈" := eq1 (at level 70) : monad_scope.
-
-(* Proof that [eq1] is an equivalence relation. *)
-Class Eq1Equivalence (M : Type -> Type) `{Monad M} `{Eq1 M} :=
-  eq1_equiv : forall A, Equivalence (eq1 (A := A)).
-
-#[global] Existing Instance eq1_equiv.
-
-Section Laws.
-
-  Context (M : Type -> Type).
-  Context {Eq1 : @Eq1 M}.
-  Context {Monad : Monad M}.
-
-  Local Open Scope monad_scope.
-
-  (* Monad laws up to [M]'s canonical equivalence relation. *)
-  (* This differs coq-ext-lib's [MonadLaws] in that the equiv. relation may be
-     distinct from [eq]. *)
-  Class MonadLawsE : Prop :=
-    { bind_ret_l : forall A B (f : A -> M B) (x : A), bind (ret x) f ≈ f x
-    ; bind_ret_r : forall A (x : M A), bind x (fun y => ret y) ≈ x
-    ; bind_bind : forall A B C (x : M A) (f : A -> M B) (g : B -> M C),
-        bind (bind x f) g ≈ bind x (fun y => bind (f y) g)
-    ; Proper_bind : forall {A B},
-        (@Proper (M A -> (A -> M B) -> M B)
-         (eq1 ==> pointwise_relation _ eq1 ==> eq1)
-         bind)
-    }.
-
-End Laws.
-
-#[global] Existing Instance Proper_bind.
-
-Arguments bind_ret_l {M _ _ _}.
-Arguments bind_ret_r {M _ _ _}.
-Arguments bind_bind {M _ _ _}.
-Arguments Proper_bind {M _ _ _}.
diff --git a/theories/Basics/MonadProp.v b/theories/Basics/MonadProp.v
index 29de11c7..20bfb681 100644
--- a/theories/Basics/MonadProp.v
+++ b/theories/Basics/MonadProp.v
@@ -4,9 +4,6 @@ From Coq Require Import
      Setoid
      Morphisms.
 
-From ExtLib Require Import
-     Structures.Monad.
-
 From ITree Require Import
      Basics.Basics
      Basics.Category
diff --git a/theories/Basics/MonadState.v b/theories/Basics/MonadState.v
index 40bee1c8..7411c663 100644
--- a/theories/Basics/MonadState.v
+++ b/theories/Basics/MonadState.v
@@ -3,17 +3,12 @@ From Coq Require Import
      Setoid
      Morphisms.
 
-From ExtLib Require Import
-     Structures.Monad.
-
 From ITree Require Import
      Basics.Basics
      Basics.Category
      Basics.CategoryKleisli
-     Basics.CategoryKleisliFacts
-     Basics.Monad.
+     Basics.CategoryKleisliFacts.
 
-Import ITree.Basics.Basics.Monads.
 Import CatNotations.
 Local Open Scope cat_scope.
 Local Open Scope cat.
@@ -22,16 +17,17 @@ Section State.
   Variable M : Type -> Type.
   Variable S : Type.
   Context {EQM : Eq1 M}.
-  Context {HM: Monad M}.
-  Context {HEQP: @Eq1Equivalence M _ EQM}.
-  Context {ML: @MonadLawsE M _ HM}.
+  Context {HR: MRet M}.
+  Context {HB: MBind M}.
+  Context {HEQP: @Eq1Equivalence M EQM}.
+  Context {ML: @MonadLawsE M EQM HR HB}.
 
-  Global Instance Eq1_stateTM : Eq1 (stateT S M).
+  #[global] Instance Eq1_stateTM : Eq1 (stateT S M).
   Proof.
     exact (fun a => pointwise_relation _ eq1).
   Defined.
 
-  Global Instance Eq1Equivalence_stateTM : @Eq1Equivalence (stateT S M) _ Eq1_stateTM.
+  #[global] Instance Eq1Equivalence_stateTM : @Eq1Equivalence (stateT S M) Eq1_stateTM.
   Proof.
   constructor.
   - repeat red.
@@ -40,30 +36,32 @@ Section State.
   - repeat red. intros. etransitivity; eauto. apply H.  apply H0.
   Qed.
 
-  Instance MonadLawsE_stateTM : @MonadLawsE (stateT S M) _ _.
+  Instance MonadLawsE_stateTM : @MonadLawsE (stateT S M) _ _ _.
   Proof.
   constructor.
-  - cbn. intros a b f x.
-    repeat red.  intros s.
+  - unfold mbind, MBind_stateT, mret, MRet_stateT.
+    intros a b f x.
+    repeat red.
+    intros s.
     rewrite bind_ret_l. reflexivity.
-  - cbn. intros a x.
+  - unfold mbind, MBind_stateT, mret, MRet_stateT.
+    intros a x.
     repeat red. intros s.
-    assert (EQM _ (bind (x s) (fun sa : S * a => ret (fst sa, snd sa))) (bind (x s) (fun sa => ret sa))).
-    { apply Proper_bind. reflexivity. intros.  repeat red. destruct a0; reflexivity. }
+    assert (EQM _ ((x s) ≫= (fun sa : S * a => mret (fst sa, snd sa))) ((x s) ≫= (fun sa => mret sa))).
+    { apply Proper_bind; [| reflexivity]. intros ?.  repeat red. destruct a0; reflexivity. }
     rewrite H.
     rewrite bind_ret_r. reflexivity.
-  - cbn. intros a b c x f g.
+  - unfold mbind, MBind_stateT, mret, MRet_stateT.
+    intros a b c x f g.
     repeat red. intros s.
     rewrite bind_bind.
-    apply Proper_bind.
-    + reflexivity.
-    + reflexivity.
+    apply Proper_bind; reflexivity.
   - repeat red. intros a b x y H x0 y0 H0 s.
     apply Proper_bind.
-    + apply H.
     + repeat red.
       destruct a0.
-      apply H0.
+      apply H.
+    + apply H0.
   Qed.
 
   Context {IM: Iter (Kleisli M) sum}.
@@ -98,7 +96,6 @@ Section State.
       apply H.
   Qed.
 
-
   Lemma internalize_cat {a b c} (f : Kleisli (stateT S M) a b) (g : Kleisli (stateT S M) b c) :
     (internalize (f >>> g)) ⩯ ((internalize f) >>> (internalize g)).
   Proof.
@@ -111,29 +108,27 @@ Section State.
     reflexivity.
   Qed.
 
-
   Lemma internalize_pure {a b c} (f : Kleisli (stateT S M) a b) (g : S * b -> S * c) :
-    internalize f >>> pure g   ⩯   (internalize (f >>> (fun b s => ret (g (s,b))))).
+    internalize f >>> pure g   ⩯   (internalize (f >>> (fun b s => mret (g (s,b))))).
   Proof.
     repeat red.
     destruct a0.
     unfold internalize, cat, Cat_Kleisli. cbn.
     apply Proper_bind; auto.
-    - reflexivity.
     - repeat red.
       destruct a1.
       unfold pure. reflexivity.
+    - reflexivity.
   Qed.
 
-
-  Global Instance Iter_stateTM : Iter (Kleisli (stateT S M)) sum.
+  #[global] Instance Iter_stateTM : Iter (Kleisli (stateT S M)) sum.
   Proof.
     exact
       (fun (a b : Type) (f : a -> S -> M (S * (a + b))) (x:a) (s:S) =>
         iter ((internalize f) >>> (pure iso)) (s, x)).
   Defined.
 
-  Global Instance Proper_Iter_stateTM : forall a b, @Proper (Kleisli (stateT S M) a (a + b) -> (Kleisli (stateT S M) a b)) (eq2 ==> eq2) iter.
+  #[global] Instance Proper_Iter_stateTM : forall a b, @Proper (Kleisli (stateT S M) a (a + b) -> (Kleisli (stateT S M) a b)) (eq2 ==> eq2) iter.
   Proof.
     destruct CM.
     repeat red.
@@ -143,33 +138,33 @@ Section State.
     destruct a1.
     cbn.
     apply Proper_bind.
-    - apply H.
     - repeat red. destruct a2 as [s' [x1|y1]]; reflexivity.
- Qed.
+    - apply H.
+  Qed.
 
-  Global Instance IterUnfold_stateTM : IterUnfold (Kleisli (stateT S M)) sum.
+  #[global] Instance IterUnfold_stateTM : IterUnfold (Kleisli (stateT S M)) sum.
   Proof.
-  destruct CM.
-  unfold IterUnfold.
-  intros a b f.
-  repeat red.
-  intros a0 s.
-  unfold cat, Cat_Kleisli.
-  unfold iter, Iter_stateTM.
-  rewrite iterative_unfold.  (* SAZ: why isn't iter_unfold exposed here? *)
-  unfold cat, Cat_Kleisli.
-  simpl.
-  rewrite bind_bind.
-  apply Proper_bind.
-  + reflexivity.
-  + repeat red. destruct a1 as [s' [x | y]]; simpl.
-    * unfold pure. rewrite bind_ret_l.
-      reflexivity.
-    * unfold pure. rewrite bind_ret_l.
-      reflexivity.
+    destruct CM.
+    unfold IterUnfold.
+    intros a b f.
+    repeat red.
+    intros a0 s.
+    unfold cat, Cat_Kleisli.
+    unfold iter, Iter_stateTM.
+    rewrite iterative_unfold.  (* SAZ: why isn't iter_unfold exposed here? *)
+    unfold cat, Cat_Kleisli.
+    simpl.
+    rewrite bind_bind.
+    apply Proper_bind.
+    + repeat red. destruct a1 as [s' [x | y]]; simpl.
+      * unfold pure. rewrite bind_ret_l.
+        reflexivity.
+      * unfold pure. rewrite bind_ret_l.
+        reflexivity.
+    + reflexivity.
   Qed.
 
-  Global Instance IterNatural_stateTM : IterNatural (Kleisli (stateT S M)) sum.
+  #[global] Instance IterNatural_stateTM : IterNatural (Kleisli (stateT S M)) sum.
   Proof.
     destruct CM.
     unfold IterNatural.
@@ -181,35 +176,27 @@ Section State.
     repeat red.
     destruct a1.
     unfold cat, Cat_Kleisli.
-    cbn.
-    rewrite! bind_bind.
-    apply Proper_bind.
-    - reflexivity.
-    - repeat red. destruct a2 as [s' [x | y]]; simpl.
-      + unfold pure. rewrite bind_ret_l.
-        cbn. unfold cat, Cat_Kleisli. cbn.
-        rewrite bind_bind.
-        rewrite bind_ret_l.
-        rewrite bind_ret_l.
-        cbn.
-        unfold id_, Id_Kleisli. unfold pure. rewrite bind_ret_l. reflexivity.
-      + unfold pure. rewrite bind_ret_l.
-        cbn. unfold cat, Cat_Kleisli. cbn.
-        rewrite bind_bind.
-        apply Proper_bind.
-        * reflexivity.
-        * repeat red. destruct a2.
-          cbn.
-          rewrite bind_ret_l. reflexivity.
+    setoid_rewrite bind_bind.
+    apply Proper_bind; [| reflexivity].
+    repeat red. destruct a2 as [s' [x | y]]; simpl.
+    + setoid_rewrite bind_ret_l; cbn.
+      setoid_rewrite bind_ret_l; cbn.
+      reflexivity.
+    + setoid_rewrite bind_ret_l; cbn.
+      setoid_rewrite bind_bind.
+      apply Proper_bind; [| reflexivity].
+      repeat red. destruct a2.
+      cbn.
+      setoid_rewrite bind_ret_l.
+      reflexivity.
   Qed.
 
   Lemma internalize_pure_iso {a b c} (f : Kleisli (stateT S M) a (b + c)) :
-    ((internalize f) >>> pure iso) ⩯ (fun sa => (bind (f (snd sa) (fst sa))) (fun sbc => ret (iso sbc))).
+    ((internalize f) >>> pure iso) ⩯ (fun sa => (f (snd sa) (fst sa)) ≫= (fun sbc => mret (iso sbc))).
   Proof.
     reflexivity.
   Qed.
 
-
   Lemma eq2_to_eq1 : forall a b (f g : Kleisli (stateT S M) a b) (x:a) (s:S),
       eq2 f g ->
       eq1 (f x s) (g x s).
@@ -218,7 +205,6 @@ Section State.
     apply H.
   Qed.
 
-
   Lemma iter_dinatural_helper:
     forall (a b c : Type) (f : Kleisli (stateT S M) a (b + c)) (g : Kleisli (stateT S M) b (a + c)),
       internalize (f >>> case_ g inr_) >>> pure iso ⩯ internalize f >>> pure iso >>> case_ (internalize g >>> pure iso) inr_.
@@ -229,23 +215,21 @@ Section State.
     destruct a0.
     unfold cat, Cat_Kleisli, internalize.
     cbn.
-    repeat rewrite bind_bind.
-    apply Proper_bind.
-    - reflexivity.
-    - repeat red.
-      destruct a1 as [s' [x | y]].
-      + unfold pure.
-        rewrite bind_ret_l.
-        unfold case_, Case_Kleisli, Function.case_sum.
-        reflexivity.
-      + unfold pure. rewrite bind_ret_l.
-        unfold case_, Case_Kleisli, Function.case_sum.
-          cbn.
-          rewrite bind_ret_l. reflexivity.
+    repeat setoid_rewrite bind_bind.
+    apply Proper_bind; [| reflexivity].
+    repeat red.
+    destruct a1 as [s' [x | y]].
+    + unfold pure.
+      rewrite bind_ret_l.
+      unfold case_, Case_Kleisli, Function.case_sum.
+      reflexivity.
+    + unfold pure. rewrite bind_ret_l.
+      unfold case_, Case_Kleisli, Function.case_sum.
+      cbn.
+      setoid_rewrite bind_ret_l. reflexivity.
   Qed.
 
-
-  Global Instance IterDinatural_stateTM : IterDinatural (Kleisli (stateT S M)) sum.
+  #[global] Instance IterDinatural_stateTM : IterDinatural (Kleisli (stateT S M)) sum.
   Proof.
     destruct CM.
     unfold IterDinatural.
@@ -260,33 +244,25 @@ Section State.
     unfold cat, Cat_Kleisli.
     rewrite bind_bind.
     unfold internalize. cbn.
-    apply Proper_bind.
-    - reflexivity.
-    - repeat red.
-      destruct a2 as [s [x | y]].
-      + unfold pure.
-        rewrite bind_ret_l.
-        cbn.
-        eapply iterative_proper_iter.
-        repeat red.
-        destruct a2.
-        cbn. rewrite! bind_bind.
-        apply Proper_bind.
-        * reflexivity.
-        * repeat red.
-          destruct a2 as [s' [x' | y]].
-          ** cbn.  rewrite bind_ret_l. unfold case_, Case_Kleisli, Function.case_sum.
-             reflexivity.
-          ** cbn.  rewrite bind_ret_l. unfold case_, Case_Kleisli, Function.case_sum.
-             rewrite bind_ret_l. reflexivity.
-      + unfold pure.
-        rewrite bind_ret_l.
-        cbn.
-        reflexivity.
-    Qed.
-
+    apply Proper_bind; [| reflexivity].
+    repeat red.
+    destruct a2 as [s [x | y]].
+    + unfold pure.
+      rewrite bind_ret_l.
+      cbn.
+      eapply iterative_proper_iter.
+      repeat red.
+      destruct a2.
+      cbn. setoid_rewrite bind_bind.
+      apply Proper_bind; [| reflexivity].
+      repeat red.
+      destruct a2 as [s' [x' | y]].
+      ** by setoid_rewrite bind_ret_l.
+      ** by setoid_rewrite bind_ret_l.
+    + by setoid_rewrite bind_ret_l.
+  Qed.
 
-  Global Instance IterCodiagonal_stateTM : IterCodiagonal (Kleisli (stateT S M)) sum.
+  #[global] Instance IterCodiagonal_stateTM : IterCodiagonal (Kleisli (stateT S M)) sum.
   Proof.
     destruct CM.
     unfold IterCodiagonal.
@@ -322,36 +298,17 @@ Section State.
    repeat rewrite bind_bind.
    unfold internalize, pure.
    cbn.
-   apply Proper_bind.
-    - reflexivity.
-    - repeat red.
-      destruct a3 as [s' [x | [y | z]]].
-      + rewrite bind_ret_l.
-        cbn. unfold id_, Id_Kleisli, pure.
-        rewrite bind_ret_l.
-        unfold cat, Cat_Kleisli.
-        rewrite bind_bind.
-        rewrite bind_ret_l.
-        cbn.  unfold inl_, Inl_Kleisli, pure.
-        rewrite bind_ret_l. reflexivity.
-      + rewrite bind_ret_l.
-        cbn.
-        rewrite bind_ret_l.
-        unfold cat, Cat_Kleisli.
-        rewrite bind_bind, bind_ret_l. cbn.
-        unfold inr_, Inr_Kleisli, pure.
-        rewrite bind_ret_l. reflexivity.
-      + rewrite bind_ret_l.
-        cbn.
-        rewrite bind_ret_l.
-        unfold cat, Cat_Kleisli.
-        rewrite bind_bind, bind_ret_l. cbn.
-        unfold inr_, Inr_Kleisli, pure.
-        rewrite bind_ret_l.
-        reflexivity.
+   apply Proper_bind; [| reflexivity].
+   repeat red.
+   destruct a3 as [s' [x | [y | z]]].
+    + setoid_rewrite bind_ret_l; cbn.
+      setoid_rewrite bind_bind; cbn.
+      by repeat setoid_rewrite bind_ret_l.
+    + by repeat setoid_rewrite bind_ret_l.
+    + by repeat setoid_rewrite bind_ret_l.
   Qed.
 
-  Global Instance Iterative_stateTM : Iterative (Kleisli (stateT S M)) sum.
+  #[global] Instance Iterative_stateTM : Iterative (Kleisli (stateT S M)) sum.
   Proof.
   constructor;
   typeclasses eauto.
diff --git a/theories/Core/ITreeDefinition.v b/theories/Core/ITreeDefinition.v
index afcf8037..2caf66eb 100644
--- a/theories/Core/ITreeDefinition.v
+++ b/theories/Core/ITreeDefinition.v
@@ -1,9 +1,6 @@
 (** * Interaction trees: core definitions *)
 
 (* begin hide *)
-Require Import ExtLib.Structures.Functor.
-Require Import ExtLib.Structures.Applicative.
-Require Import ExtLib.Structures.Monad.
 Require Import Program.Tactics.
 
 From ITree Require Import Basics.
@@ -163,9 +160,10 @@ Definition subst {E : Type -> Type} {T U : Type} (k : T -> itree E U)
     | VisF e h => Vis e (fun x => _subst (h x))
     end.
 
-Definition bind {E : Type -> Type} {T U : Type} (u : itree E T) (k : T -> itree E U)
-  : itree E U :=
-  subst k u.
+Notation bind u k := (subst k u).
+(* Definition bind {E : Type -> Type} {T U : Type} (u : itree E T) (k : T -> itree E U) *)
+(*   : itree E U := *)
+(*   subst k u. *)
 
 (** Monadic composition of continuations (i.e., Kleisli composition).
  *)
@@ -224,9 +222,9 @@ Ltac fold_subst :=
   repeat (change (ITree.subst ?k ?t) with (ITree.bind t k)).
 
 Ltac fold_monad :=
-  repeat (change (@ITree.bind ?E) with (@Monad.bind (itree E) _));
-  repeat (change (go (@RetF ?E _ _ _ ?r)) with (@Monad.ret (itree E) _ _ r));
-  repeat (change (@ITree.map ?E) with (@Functor.fmap (itree E) _)).
+  repeat (change (@ITree.subst ?E) with (@mbind (itree E) _));
+  repeat (change (go (@RetF ?E _ _ _ ?r)) with (@mret (itree E) _ _ r));
+  repeat (change (@ITree.map ?E) with (@fmap (itree E) _)).
 
 End ITree.
 
@@ -242,36 +240,28 @@ End ITree.
  *)
 
 Module ITreeNotations.
-Notation "t1 >>= k2" := (ITree.bind t1 k2)
-  (at level 58, left associativity) : itree_scope.
-Notation "x <- t1 ;; t2" := (ITree.bind t1 (fun x => t2))
-  (at level 61, t1 at next level, right associativity) : itree_scope.
-Notation "t1 ;; t2" := (ITree.bind t1 (fun _ => t2))
-  (at level 61, right associativity) : itree_scope.
-Notation "' p <- t1 ;; t2" :=
-  (ITree.bind t1 (fun x_ => match x_ with p => t2 end))
-  (at level 61, t1 at next level, p pattern, right associativity) : itree_scope.
-Infix ">=>" := ITree.cat (at level 61, right associativity) : itree_scope.
+Notation "t1 ≫= k2" := (ITree.subst k2 t1) : itree_scope.
+Notation "x ← t1 ; t2" := (ITree.subst (fun x => t2) t1) : itree_scope.
+Notation "t1 ;; t2" := (ITree.subst (fun _ => t2) t1) : itree_scope.
+Notation "' p ← t1 ; t2" :=
+  (ITree.subst (fun x_ => match x_ with p => t2 end) t1)
+  (at level 20, p pattern, t1 at level 100, t2 at level 200, only parsing) : itree_scope.
+Infix ">=>" := ITree.cat (at level 60, right associativity) : itree_scope.
 End ITreeNotations.
 
 (** ** Instances *)
 
-#[global] Instance Functor_itree {E} : Functor (itree E) :=
-{ fmap := @ITree.map E }.
+#[global] Instance FMap_itree {E} : FMap (itree E) := @ITree.map E.
 
 (* Instead of [pure := @Ret E], [ret := @Ret E], we eta-expand
    [pure] and [ret] to make the extracted code respect OCaml's
    value restriction. *)
-#[global] Instance Applicative_itree {E} : Applicative (itree E) :=
-{ pure := fun _ x => Ret x
-; ap := fun _ _ f x =>
-          ITree.bind f (fun f => ITree.bind x (fun x => Ret (f x)))
-}.
-
-#[global] Instance Monad_itree {E} : Monad (itree E) :=
-{| ret := fun _ x => Ret x
-;  bind := @ITree.bind E
-|}.
+#[global] Instance Applicative_itree {E} : App (itree E) :=
+  fun _ _ f x => ITree.bind f (fun f => ITree.bind x (fun x => Ret (f x))).
+
+#[global] Instance MRet_itree {E} : MRet (itree E) := fun _ x => Ret x.
+
+#[global] Instance MBind_itree {E} : MBind (itree E) := @ITree.subst E.
 
 #[global] Instance MonadIter_itree {E} : MonadIter (itree E) :=
   fun _ _ => ITree.iter.
diff --git a/theories/Core/ITreeMonad.v b/theories/Core/ITreeMonad.v
index 8e272245..966119ef 100644
--- a/theories/Core/ITreeMonad.v
+++ b/theories/Core/ITreeMonad.v
@@ -5,7 +5,6 @@
 
 From ITree Require Import
      Basics.Basics
-     Basics.Monad
      Core.ITreeDefinition
      Eq.Eqit
      Eq.UpToTaus.
@@ -26,14 +25,12 @@ Instance MonadLawsE_ITree {E} : MonadLawsE (itree E).
 Proof.
   constructor.
   - intros a b f x.
-    unfold Monad.bind, Monad.ret, Monad_itree.
-    unfold eq1, Eq1_ITree. rewrite bind_ret_l. reflexivity.
-  - intros a x.    unfold Monad.bind, Monad.ret, Monad_itree.
-    unfold eq1, Eq1_ITree. rewrite bind_ret_r. reflexivity.
-  - intros a b c x f g. unfold Monad.bind, Monad.ret, Monad_itree.
-    unfold eq1, Eq1_ITree. rewrite bind_bind. reflexivity.
-  - unfold Monad.bind, Monad_itree.
-    intros.
+    by setoid_rewrite bind_ret_l.
+  - intros a x.
+    by setoid_rewrite bind_ret_r.
+  - intros a b c x f g.
+    by setoid_rewrite bind_bind.
+  - intros.
     repeat red.
     intros.
     apply eqit_bind; auto.
diff --git a/theories/Core/KTree.v b/theories/Core/KTree.v
index 64a2e12a..88964142 100644
--- a/theories/Core/KTree.v
+++ b/theories/Core/KTree.v
@@ -10,7 +10,6 @@ From ITree Require Import
      Basics.Basics
      Basics.CategoryOps
      Basics.CategoryKleisli
-     Basics.Monad
      Basics.CategoryKleisli
      Basics.Function
      Core.ITreeDefinition
diff --git a/theories/Core/KTreeFacts.v b/theories/Core/KTreeFacts.v
index a84858e8..e0561149 100644
--- a/theories/Core/KTreeFacts.v
+++ b/theories/Core/KTreeFacts.v
@@ -31,7 +31,6 @@ Local Open Scope cat_scope.
 
 Ltac unfold_ktree :=
   unfold
-    Monad.eq1, Eq1_ITree,
     Basics.iter, MonadIter_itree,
     assoc_l, AssocL_Coproduct,
     bimap, Bimap_Coproduct,
@@ -139,7 +138,6 @@ Qed.
           (iter (C := ktree E)).
 Proof.
   intros body1 body2 EQ_BODY a. repeat red in EQ_BODY.
-  unfold_ktree.
   eapply (eq_itree_iter' eq); auto.
   intros; eapply eqit_mon, EQ_BODY; auto.
   intros [] _ []; auto; econstructor; subst; auto.
@@ -151,7 +149,6 @@ Qed.
           (iter (C := ktree E)).
 Proof.
   intros body1 body2 EQ_BODY a. repeat red in EQ_BODY.
-  unfold_ktree.
   eapply (eutt_iter' eq); auto.
   intros ? _ []; eapply eqit_mon, EQ_BODY; auto.
   intros [] _ []; auto; econstructor; auto.
@@ -188,22 +185,23 @@ Qed.
 
 #[global] Instance IterUnfold_ktree {E} : IterUnfold (ktree E) sum.
 Proof.
-  repeat intro. unfold_ktree. rewrite unfold_iter_ktree.
+  repeat intro. rewrite unfold_iter_ktree.
   eapply eutt_clo_bind; try reflexivity.
   intros [] ? []; try rewrite tau_eutt; reflexivity.
 Qed.
 
 #[global] Instance IterNatural_ktree {E} : IterNatural (ktree E) sum.
 Proof.
-  repeat intro. unfold_ktree.
+  repeat intro.
   revert a0.
   einit. ecofix CIH. intros.
+  unfold_ktree.
   rewrite 2 unfold_iter_ktree.
-  rewrite !bind_bind.
+  repeat setoid_rewrite bind_bind.
   ebind; econstructor; try reflexivity.
   intros [] ? [].
-  - rewrite bind_tau, 2 bind_ret_l. etau.
-  - rewrite bind_ret_l, !bind_bind. setoid_rewrite bind_ret_l. rewrite bind_ret_r.
+  - setoid_rewrite bind_tau. do 2 setoid_rewrite bind_ret_l. etau.
+  - setoid_rewrite bind_ret_l; repeat setoid_rewrite bind_bind. setoid_rewrite bind_ret_l. rewrite bind_ret_r.
     reflexivity.
 Qed.
 
@@ -327,51 +325,62 @@ Proof.
   split; typeclasses eauto.
 Qed.
 
+CoInductive stream := | cons : nat -> stream -> stream.
+
+(* CoFixpoint zeros := cons 0 zeros. *)
+
+(* Goal zeros = zeros. *)
+(* cbn. *)
+Import ITreeNotations.
 (* Equation merging the sequence of two [iter] into one *)
-Lemma cat_iter: 
-  forall {E: Type -> Type} {a b c} (f: ktree E a (a + b)) (g: ktree E b (b + c)), 
+Lemma cat_iter:
+  forall {E: Type -> Type} {a b c} (f: ktree E a (a + b)) (g: ktree E b (b + c)),
     ITree.iter f >>> ITree.iter g ⩯ inl_ >>> ITree.iter (case_ (f >>> inl_) (g >>> inr_ >>> assoc_l)).
 Proof.
   intros *.
-  unfold_ktree.
+  unfold
+    Basics.iter, MonadIter_itree,
+    assoc_l, AssocL_Coproduct,
+    bimap, Bimap_Coproduct,
+    cat, Cat_Kleisli, inl_, Inl_Kleisli, inr_, Inr_Kleisli, case_, Case_Kleisli, case_sum,
+    lift_ktree_, mbind, MBind_itree.
   (* We move to the eworld *)
   einit.
-  intros.
-  revert a0.
   (* First coinductive point in the simulation: at the entry point of the iteration over f *)
   ecofix CIH.
   intros.
-  cbn.
-  rewrite bind_ret_l.
+  setoid_rewrite bind_ret_l.
   (* We unfold one step on both sides *)
   match goal with
   |- euttG _ _ _ _ _ ?t _ => remember t; rewrite unfold_iter; subst
   end.
   rewrite unfold_iter; cbn.
-  rewrite !bind_bind.
+  repeat setoid_rewrite bind_bind.
   ebind.
   (* We run f a first time on both side *)
   econstructor; [reflexivity | intros [xa | xb] ? <-].
   - (* If we loop back to f, we can conclude by coinduction *)
-    rewrite ! bind_ret_l.
+    repeat setoid_rewrite bind_ret_l.
     rewrite bind_tau.
     etau.
     specialize (CIHL xa). cbn in CIHL.
     match goal with
       |- euttG _ _ _ _ _ ?t _ => remember t
     end.
-    rewrite <- bind_ret_l.
+    clear CIHH.
+    (* rewrite <- bind_ret_l. *)
     ebase.
+    right. apply CIHL.
   - (* If we exit the first loop *)
-    rewrite ! bind_ret_l.
+    setoid_rewrite bind_ret_l.
     (* We setup a second coinductive point in the simulation.
        We just make sure to first get rid of the additional tau guard
-       that we have encountered in the right of the equation to keep the second part clean. 
+       that we have encountered in the right of the equation to keep the second part clean.
      *)
     rewrite tau_euttge.
     generalize xb.
     ecofix CIH'.
-    
+
     intros ?.
     (* We unfold a new step of computation *)
     rewrite unfold_iter; cbn.
diff --git a/theories/Eq/Eqit.v b/theories/Eq/Eqit.v
index 9ec83997..56308538 100644
--- a/theories/Eq/Eqit.v
+++ b/theories/Eq/Eqit.v
@@ -34,6 +34,7 @@ From ITree Require Import
      Eq.Paco2
      Eq.Shallow.
 
+
 Local Open Scope itree_scope.
 
 (* TODO: Send to paco *)
@@ -64,8 +65,6 @@ Proof. auto. Qed.
     instead encoding a form of productivity visibly in types.
  *)
 
-Local Coercion is_true : bool >-> Sortclass.
-
 Section eqit.
 
   (** Although the original motivation is to define an equivalence
@@ -628,7 +627,7 @@ Lemma eqitree_inv_Vis_r {E R U} (t : itree E R) (e : E U) (k : U -> _) :
   t ≅ Vis e k -> exists k', observe t = VisF e k' /\ forall u, k' u ≅ k u.
 Proof.
   intros; punfold H; apply eqitF_inv_VisF_r in H.
-  destruct H as [ [? [-> ?]] | [] ]; [ | discriminate ].
+  destruct H as [ [? [-> ?]] | [] ]; [ | easy ].
   pclearbot. eexists; split; eauto.
 Qed.
 
@@ -692,7 +691,7 @@ Proof with eauto with itree.
   intros. punfold H. red in H. simpl in *.
   remember (TauF t1) as tt1. remember (TauF t2) as tt2.
   hinduction H before b2; intros; try discriminate.
-  - inv Heqtt1. inv Heqtt2. pclearbot. eauto.
+  - inv Heqtt1. pclearbot. eauto.
   - inv Heqtt1. inv H.
     + pclearbot. punfold REL. pstep. red. simpobs...
     + pstep. red. simpobs. econstructor; eauto. pstep_reverse. apply IHeqitF; eauto.
@@ -730,10 +729,11 @@ Proof.
   genobs t1 ot1; genobs t2 ot2; revert t1 t2 Heqot1 Heqot2; unfold observe, _observe.
   destruct H; pclearbot; intros * E1 E2; rewrite <- E1, <- E2; cbn; auto.
   - exists eq_refl; cbn; eauto.
-  - rewrite CHECK in *. destruct ot2.
+  - destruct b1; try done.
+    case_match.
     1,3: pfold; red; unfold observe, _observe; rewrite <- E2; assumption.
     1: apply eqit_inv_Tau_r; pfold; red; unfold observe, _observe; assumption.
-  - rewrite CHECK in *. destruct ot1.
+  - destruct b2; try done; case_match.
     1,3: pfold; red; unfold observe, _observe; rewrite <- E1; assumption.
     1: apply eqit_inv_Tau_l; pfold; red; unfold observe, _observe; assumption.
 Qed.
@@ -876,8 +876,8 @@ Qed.
          (gpaco2 (@eqit_ E R1 R2 RS b1 b2 id) (eqitC RS b1 b2) r rg).
 Proof.
   repeat intro. guclo eqit_clo_trans. econstructor; cycle -3; eauto.
-  - eapply eqit_mon, H; eauto; discriminate.
-  - eapply eqit_mon, H0; eauto; discriminate.
+  - by eapply eqit_mon, H.
+  - by eapply eqit_mon, H0.
 Qed.
 
 #[global] Instance geuttgen_cong_eqit_eq {E R1 R2 RS} b1 b2 r rg:
@@ -1124,11 +1124,11 @@ Proof.
     eauto with paco.
   - gstep. econstructor. eauto 7 with paco itree.
   - gstep. econstructor. intros. red in CMP. unfold id in ID. apply ID. eauto 7 with paco itree.
-  - destruct b1; try discriminate.
+  - destruct b1; try done.
     guclo eqit_clo_trans.
     econstructor; auto_ctrans_eq; eauto; try reflexivity.
     eapply eqit_Tau_l. rewrite unfold_bind. reflexivity.
-  - destruct b2; try discriminate.
+  - destruct b2; try done.
     guclo eqit_clo_trans. econstructor; auto_ctrans_eq; eauto; try reflexivity.
     eapply eqit_Tau_l. rewrite unfold_bind. reflexivity.
 Qed.
@@ -1187,8 +1187,8 @@ Proof.
 Qed.
 
 #[global] Instance eqit_bind {E R S} b1 b2 :
-  Proper (eqit eq b1 b2 ==> pointwise_relation _ (eqit eq b1 b2) ==>
-          eqit eq b1 b2) (@ITree.bind E R S).
+  Proper (pointwise_relation _ (eqit eq b1 b2) ==> eqit eq b1 b2 ==>
+          eqit eq b1 b2) (@ITree.subst E R S).
 Proof.
   repeat intro; eapply eqit_bind'; eauto.
   intros; subst; auto.
@@ -1229,8 +1229,8 @@ Lemma bind_ret_r' {E R} (u : itree E R) (f : R -> R) :
   ITree.bind u (fun r => Ret (f r)) ≅ u.
 Proof.
   intro H. rewrite <- (bind_ret_r u) at 2. apply eqit_bind.
-  - reflexivity.
   - hnf. intros. apply eqit_Ret. auto.
+  - reflexivity.
 Qed.
 
 Lemma bind_bind {E R S T} :
diff --git a/theories/Eq/Rutt.v b/theories/Eq/Rutt.v
index c7e7d0f2..35303150 100644
--- a/theories/Eq/Rutt.v
+++ b/theories/Eq/Rutt.v
@@ -19,9 +19,6 @@ From Coq Require Import
      Morphisms
 .
 
-From ExtLib Require Import
-     Structures.Monad.
-
 From ITree Require Import
      Basics.Utils
      Axioms
diff --git a/theories/Eq/Shallow.v b/theories/Eq/Shallow.v
index 8cfa2411..05a3525a 100644
--- a/theories/Eq/Shallow.v
+++ b/theories/Eq/Shallow.v
@@ -110,10 +110,10 @@ Proof. reflexivity. Qed.
 
 #[global]
 Instance observing_bind {E R S} :
-  Proper (observing eq ==> eq ==> observing eq) (@ITree.bind E R S).
+  Proper (eq ==> observing eq ==> observing eq) (@ITree.subst E R S).
 Proof.
   repeat intro; subst. constructor. unfold observe. cbn.
-  rewrite (observing_observe H). reflexivity.
+  rewrite (observing_observe H0). reflexivity.
 Qed.
 
 Lemma bind_ret_ {E R S} (r : R) (k : R -> itree E S) :
diff --git a/theories/Eq/SimUpToTaus.v b/theories/Eq/SimUpToTaus.v
index 4210985b..17fb52b8 100644
--- a/theories/Eq/SimUpToTaus.v
+++ b/theories/Eq/SimUpToTaus.v
@@ -210,14 +210,14 @@ Proof.
   punfold H0; punfold H1; punfold H2. red in H0, H1.
   (* rename H1 into H2, Hxy into H1.  *)
   hinduction H2 before CIH; subst; intros.
-  - inv H0; try discriminate. inv H1; try discriminate. econstructor. eauto.
-  - dependent destruction H0; try discriminate.
-    dependent destruction H1; try discriminate.
+  - inv H0; try easy. inv H1; try easy. econstructor. eauto.
+  - dependent destruction H0; try easy.
+    dependent destruction H1; try easy.
     simpobs. pclearbot.
     constructor. intros. right. eauto 7 with paco itree.
-  - dependent destruction H1; try discriminate.
+  - dependent destruction H1; try easy.
     simpobs. pclearbot. punfold REL. auto with itree.
-  - dependent destruction H0; try discriminate.
+  - dependent destruction H0; try easy.
     simpobs. pclearbot. constructor.
     right. rewrite (itree_eta' ot2) in *. eauto with itree.
 Qed.
diff --git a/theories/Eq/UpToTaus.v b/theories/Eq/UpToTaus.v
index 325220b5..847c16f7 100644
--- a/theories/Eq/UpToTaus.v
+++ b/theories/Eq/UpToTaus.v
@@ -48,6 +48,9 @@ From ITree Require Import
 #[local] Open Scope itree_scope.
 (* end hide *)
 
+(* The standard library has specialized instances of `Equivalence eq` at specific types, which leads to abuse instantiations of evars. We make sure to find [eq_equivalence] first *)
+Existing Instance eq_equivalence.
+
 (** ** gpaco
 *)
 
@@ -330,7 +333,9 @@ Proof.
     hinduction REL0 before CIH; intros; subst.
     + apply eqit_ret_gen in REL0.
       gclo. econstructor.
-      * eapply eqit_trans; [rewrite (simpobs Heqot1); reflexivity|].
+      * eapply eqit_trans.
+        (* This is bugged, instantiate abusively an evar *)
+        rewrite (simpobs Heqot1). reflexivity.
         eapply eqit_trans; [rewrite tau_euttge; reflexivity|].
         eauto.
       * rewrite (simpobs Heqot2). reflexivity.