diff --git a/.github/workflows/coq.yml b/.github/workflows/coq.yml
index 2cd7ea3..d827a39 100644
--- a/.github/workflows/coq.yml
+++ b/.github/workflows/coq.yml
@@ -14,19 +14,27 @@ jobs:
     strategy:
       matrix:
         coq_version:
-          - '8.15.2'
+          - '9.2'
         ocaml_version:
-          - '4.14.0-flambda'
+          - '4.14-flambda'
       max-parallel: 4
       fail-fast: false
 
     steps:
-      - uses: actions/checkout@v2
+      - uses: actions/checkout@v4
       - uses: coq-community/docker-coq-action@v1
         with:
-          opam_file: 'coq-ctree.opam'
+          opam_file: 'rocq-ctree.opam'
           coq_version: ${{ matrix.coq_version }}
           ocaml_version: ${{ matrix.ocaml_version }}
+          before_install: |
+            sudo chown -R "$(id -u):$(id -g)" .
+            opam pin remove -n -y dune
+            opam update -y
+            opam install -y dune.3.23.1
+            dune build rocq-ctree.opam
+            cp _build/default/rocq-ctree.opam .
+          before_script: dune build -j 2
           export: 'OPAMWITHTEST'
         env:
           OPAMWITHTEST: 'true'
diff --git a/README.md b/README.md
index cad7de0..c3331b3 100644
--- a/README.md
+++ b/README.md
@@ -14,7 +14,7 @@ We develop a cousin of Interaction Trees, dubbed _Choice Trees_, with native sup
   - Yannick Zakowski
   - Steve Zdancewic
 - License: MIT License
-- Compatible Rocq versions: 9.0
+- Compatible Rocq versions: 9.2
 - Additional dependencies:
   - dune
   - [Extlib](https://github.com/coq-community/coq-ext-lib)
@@ -51,9 +51,12 @@ cd ctrees
 dune build
 ```
 
-## Universe issue
+## Universe checking
 
-We currently unset locally universe checking in several places of the library. This is an annoying, but purely technical issue that affects in no way the soundness of our results.
+Universe checking remains enabled throughout the library. The former
+inconsistency came from monomorphic universe instances that identified event
+and branch indices with the higher universes needed by nested choice trees,
+state transformers, and interpreters. These declarations now keep their
+universe levels independent and polymorphic.
 
-Given the complexity of the issue, and its root tracing back to other libraries (for instance, importing simultaneously some parts of the [Interaction Tree] library and of the [RelationAlgebra] library triggers a universe inconsistency), we project to tackle the issue as part of the future support in Rocq for algebraic universes and the release of a universe polymorphic prelude.
 
diff --git a/dune-project b/dune-project
index 355cb7e..25a6fe5 100644
--- a/dune-project
+++ b/dune-project
@@ -1,5 +1,5 @@
-(lang dune 3.8)
-(using coq 0.7)
+(lang dune 3.23)
+(using rocq 0.11)
 (name rocq-ctree)
 
 (license "MIT")
@@ -15,11 +15,11 @@
  (synopsis "Library for representing recursive, non-deterministic and impure programs with equational reasoning")
  (version 2.0-dev)
  (depends
-  (rocq-core (>= 9.0))
+  (rocq-core (>= 9.2))
   (rocq-stdlib (>= 9.0))
   (coq-ext-lib (>= 0.11.3))
   (rocq-coinduction (>= 1.21))
-  (rocq-relation-algebra (>= 1.8.0))
+  (rocq-relation-algebra (>= 1.9.0))
   (rocq-equations (>= 1.3.1))
   (coq-itree (>= 5.0)))
  (tags (
diff --git a/examples/AltBisim/dune b/examples/AltBisim/dune
index d9a93f4..c005e6f 100644
--- a/examples/AltBisim/dune
+++ b/examples/AltBisim/dune
@@ -1,4 +1,4 @@
-(coq.theory
+(rocq.theory
  (name CTreeBisimExample)
  (theories CTree)
 )
diff --git a/examples/CCS/Denotation.v b/examples/CCS/Denotation.v
index 902db66..b0de514 100644
--- a/examples/CCS/Denotation.v
+++ b/examples/CCS/Denotation.v
@@ -5,7 +5,6 @@ Denotation of [ccs] into [ctree]s
 
 .. coq:: none
 |*)
-Unset Universe Checking.
 
 From Stdlib Require Export
      List
@@ -53,8 +52,9 @@ Variant ActionE : Type -> Type :=
 Notation ccsE := ActionE.
 Notation ccsC := (B2 +' B3 +' B4).
 
-Definition ccsT' T := ctree' ccsE ccsC T.
-Definition ccsT := ctree ccsE ccsC.
+Universe ccs_u.
+Definition ccsT := @ctree@{_ _ _ _ ccs_u ccs_u} ccsE ccsC.
+Definition ccsT' (T : Type@{ccs_u}) := ctreeF ccsE ccsC T (ccsT T).
 
 Definition ccs' := ccsT' void.
 Definition ccs  := ccsT void.
@@ -71,7 +71,7 @@ Section Combinators.
 
   Definition plus (P Q : ccs) : ccs := br2 P Q.
 
-  Definition h_new (c : chan) : ActionE ~> ctree ccsE ccsC :=
+  Definition h_new (c : chan) : ActionE ~> ccsT :=
     fun _ e => let '(Act a) := e in
             match a with
             | Send c'
@@ -81,7 +81,7 @@ Section Combinators.
   #[global] Arguments h_new c [T] _.
 
   Definition new : chan -> ccs -> ccs :=
-    fun c P => interp (h_new c) P.
+    fun c P => interp (M := @ctree@{_ _ _ _ ccs_u ccs_u} ccsE ccsC) (h_new c) P.
 
   Definition para : ccs -> ccs -> ccs :=
     cofix F (P : ccs) (Q : ccs) :=
@@ -237,7 +237,7 @@ Proof.
     rewrite <- eq1; eauto.
 Qed.
 
-Lemma trans_brS' {E C X Y} : forall (c : C Y) (k : Y -> ctree E C X) x u,
+Polymorphic Lemma trans_brS' {E C X Y} : forall (c : C Y) (k : Y -> ctree E C X) x u,
     u ≅ k x ->
 		trans τ (BrS c k) u.
 Proof.
@@ -262,15 +262,17 @@ Qed.
 (* TO MOVE *)
 Ltac ssplit := split; [| split].
 Ltac eex := do 2 eexists.
-Lemma trans_trigger_inv' : forall {E C X} (e : E X) l u,
-		trans l (trigger e : ctree E C X) u ->
-    exists x, u ≅ Ret x /\ l = obs e x.
+Polymorphic Lemma trans_trigger_inv'@{d q +} : forall
+    {E : Type -> Type} {C : Type -> Type} {X : Type} (e : E X) l
+    (u : @ctree@{_ _ _ _ d q} E C X),
+    trans l (trigger e : @ctree@{_ _ _ _ d q} E C X) u ->
+    exists x, u ≅ (Ret x : @ctree@{_ _ _ _ d q} E C X) /\ l = obs e x.
 Proof.
   intros * TR.
-  unfold trigger in TR.
+  rewrite Equ.unfold_trigger in TR.
   now apply trans_vis_inv in TR.
 Qed.
-Lemma trans_vis' {E C R X} : forall (e : E X) x (k : X -> ctree E C R) u,
+Polymorphic Lemma trans_vis' {E C R X} : forall (e : E X) x (k : X -> ctree E C R) u,
     u ≅ k x ->
     trans (obs e x) (Vis e k) u.
 Proof.
@@ -290,12 +292,14 @@ Definition can_comm (c : chan) (a : @label ccsE) : bool :=
 
 Lemma trans_hnew_inv : forall a l c p,
     trans l (h_new c (Act a)) p ->
-    l = obs (Act a) tt /\ can_comm c l /\ p ≅ Ret tt.
+    l = obs (Act a) tt /\ can_comm c l /\ p ≅ (Ret tt : ccsT unit).
 Proof.
   intros * tr.
-  cbn in *; destruct a; cbn in *; destruct (c =? c0) eqn:comm; cbn in *.
+  destruct a; cbn [h_new] in tr;
+    destruct (c =? c0) eqn:comm; cbn [h_new] in tr.
   all : try now eapply Stuck_is_stuck in tr.
-  all: unfold can_comm; apply trans_trigger_inv' in tr as ([] & ? & ?); subst; rewrite comm; eauto.
+  all: unfold can_comm; apply trans_trigger_inv' in tr as ([] & EQ & ->);
+    rewrite comm; auto.
 Qed.
 
 Lemma new_guard : forall c t, new c (Guard t) ≅ Guard (new c t).
@@ -373,9 +377,9 @@ Proof.
   - tauto.
 Qed.
 
-Lemma trans_new_inv_aux : forall l T U,
+Lemma trans_new_inv_aux : forall l (T U : ccs'),
     trans_ l T U ->
-    forall c p q,
+    forall c (p q : ccs),
       (go T ≅ new c p \/ go T ≅ Guard (new c p)) ->
       go U ≅ q ->
       exists q', can_comm c l = true /\ trans l p q' /\
@@ -387,22 +391,17 @@ Proof.
   - destruct EQ1 as [EQ1 | EQ1].
     + unfold new in EQ1; rewrite unfold_interp in EQ1.
       unfold trans, transR.
-      cbn.
+      cbn -[CTree.branch MonadBr_ctree].
       desobs p; try now (step in EQ1; inv EQ1).
-      * destruct e,a; cbn in *.
-        ** destruct (c =? c1); cbn in *.
-           *** step in EQ1; dependent induction EQ1; inv x0.
-           *** step in EQ1; inv EQ1.
-        ** destruct (c =? c1); cbn in *.
-           *** step in EQ1; dependent induction EQ1; inv x0.
-           *** step in EQ1; inv EQ1.
-      * cbn in EQ1.
-        unfold Utils.mbr, MonadBr_ctree, branch in EQ1.
-        cbn in * |-.
-        rewrite unfold_bind in EQ1; cbn in EQ1.
+      * destruct e,a; cbn [h_new] in EQ1;
+          destruct (c =? c1); cbn [h_new] in EQ1;
+          try solve [step in EQ1; dependent induction EQ1; inv x0];
+          rewrite bind_trigger in EQ1; step in EQ1; inv EQ1.
+      * cbn -[CTree.branch MonadBr_ctree] in EQ1.
+        unfold Utils.mbr, MonadBr_ctree in EQ1; rewrite bind_branch in EQ1.
         inv_equ. rename EQ into eqx.
         specialize (eqx x).
-        cbn in * |-; rewrite bind_ret_l in eqx.
+        cbn -[CTree.trigger CTree.bind] in * |-.
         edestruct (IHtr (k0 x)) as (q' & comm & tr' & EQ).
         now right; rewrite <- ctree_eta.
         eauto.
@@ -415,7 +414,7 @@ Proof.
   - destruct EQ1 as [EQ1 | EQ1].
     + unfold new in EQ1; rewrite unfold_interp in EQ1.
       unfold trans, transR.
-      cbn.
+      cbn -[CTree.trigger CTree.bind].
       desobs p; try now (step in EQ1; inv EQ1).
       * inv_equ.
         edestruct (IHtr t0) as (q' & comm & tr' & EQ).
@@ -425,13 +424,10 @@ Proof.
         eexists; ssplit; auto.
         econstructor; apply tr'.
         rewrite <- EQ2; eauto.
-      * destruct e,a; cbn in *.
-        ** destruct (c =? c0); cbn in *.
-           *** step in EQ1; dependent induction EQ1; inv x0.
-           *** step in EQ1; inv EQ1.
-        ** destruct (c =? c0); cbn in *.
-           *** step in EQ1; dependent induction EQ1; inv x0.
-           *** step in EQ1; inv EQ1.
+      * destruct e,a; cbn [h_new] in EQ1;
+          destruct (c =? c0); cbn [h_new] in EQ1;
+          try solve [step in EQ1; dependent induction EQ1; inv x0];
+          rewrite bind_trigger in EQ1; step in EQ1; inv EQ1.
     + inv_equ.
       edestruct IHtr as (q' & comm & tr' & EQ).
       left; rewrite EQ1, <- ctree_eta; reflexivity.
@@ -442,46 +438,47 @@ Proof.
   - destruct EQ1 as [EQ1 | EQ1]; inv_equ.
     + unfold new in EQ1; rewrite unfold_interp in EQ1.
       unfold trans, transR.
-      cbn.
+      cbn -[CTree.trigger CTree.bind].
       desobs p; try now (step in EQ1; inv EQ1).
       * inv_equ.
         eexists; ssplit; auto.
         constructor; reflexivity.
         rewrite <- EQ2, <- ctree_eta, H; auto.
-      * destruct e,a; cbn in *.
-        ** destruct (c =? c0); cbn in *.
-           *** step in EQ1; dependent induction EQ1; inv x0.
-           *** step in EQ1; inv EQ1.
-        ** destruct (c =? c0); cbn in *.
-           *** step in EQ1; dependent induction EQ1; inv x0.
-           *** step in EQ1; inv EQ1.
+      * destruct e,a; cbn [h_new] in EQ1;
+          destruct (c =? c0); cbn [h_new] in EQ1;
+          try solve [step in EQ1; dependent induction EQ1; inv x0];
+          rewrite bind_trigger in EQ1; step in EQ1; inv EQ1.
 
   - destruct EQ1 as [EQ1 | EQ1]; [ | inv_equ].
-    unfold new in EQ1; rewrite unfold_interp in EQ1.
-    unfold trans,transR; cbn.
-    desobs p; inv_equ.
-    cbn in *.
-    destruct e0,a; cbn in *; destruct (c =? c0) eqn:EQ; inv_equ.
-    + rewrite bind_trigger in EQ1.
-      inv_equ.
-      rewrite EQ; eexists; ssplit; auto.
-      constructor; reflexivity.
-      rewrite <- EQ2, <- ctree_eta, <- H; auto.
-    + rewrite bind_trigger in EQ1.
-      inv_equ.
-      rewrite EQ; eexists; ssplit; auto.
-      constructor; reflexivity.
-      rewrite <- EQ2, <- ctree_eta, <- H; auto.
+    unfold new in EQ1.
+    destruct (observe p) as [r | | t0 | t0 | U0 e0 k0 | U0 c0 k0] eqn:EP;
+      rewrite (ctree_eta p), EP in EQ1.
+    + destruct r.
+    + rewrite FoldCTree.interp_stuck in EQ1; inv_equ.
+    + rewrite FoldCTree.interp_step in EQ1; inv_equ.
+    + rewrite FoldCTree.interp_guard in EQ1; inv_equ.
+    + rewrite FoldCTree.interp_vis in EQ1.
+      destruct e0 as [a]; destruct a as [ch | ch];
+        cbn [h_new] in EQ1;
+        destruct (c =? ch) eqn:COMM.
+      all: try solve [rewrite bind_stuck in EQ1; inv_equ].
+      all: pose proof (trans_vis e x k) as TR.
+      all: rewrite H, EQ1 in TR;
+        apply Trans.trans_trigger_inv in TR as ([] & ET & EL).
+      all: exists (k0 tt); ssplit.
+      all: try solve [rewrite EL; cbn [can_comm]; rewrite COMM; reflexivity].
+      all: try solve [rewrite EL, (ctree_eta p), EP; apply trans_vis].
+      all: rewrite <- EQ2, <- ctree_eta; exact ET.
+    + rewrite FoldCTree.interp_br' in EQ1; inv_equ.
 
  - destruct EQ1 as [EQ1 | EQ1]; inv_equ.
    unfold new in EQ1; rewrite unfold_interp in EQ1.
-   unfold trans,transR; cbn.
+   unfold trans,transR; cbn -[CTree.trigger CTree.bind].
    desobs p; inv_equ.
    destruct r0.
-   cbn in *.
-   destruct e,a; cbn in *.
-   * destruct (c =? c0); cbn in *; inv_equ.
-   * destruct (c =? c0); cbn in *; inv_equ.
+   destruct e,a; cbn [h_new] in EQ1;
+     destruct (c =? c0); cbn [h_new] in EQ1;
+     rewrite ?bind_trigger in EQ1; inv_equ.
 Qed.
 
 Lemma trans_new_inv : forall l c p p',
diff --git a/examples/CCS/OpDenot.v b/examples/CCS/OpDenot.v
index 86917a9..320911a 100644
--- a/examples/CCS/OpDenot.v
+++ b/examples/CCS/OpDenot.v
@@ -1,4 +1,3 @@
-Unset Universe Checking.
 
 From CTree Require Import
      CTree
diff --git a/examples/CCS/dune b/examples/CCS/dune
index 047c96f..1f5ea64 100644
--- a/examples/CCS/dune
+++ b/examples/CCS/dune
@@ -1,4 +1,4 @@
-(coq.theory
+(rocq.theory
   (name CTreeCCS)
   (theories CTree)
 )
\ No newline at end of file
diff --git a/examples/Coffee/dune b/examples/Coffee/dune
index 326b5e3..e0163c3 100644
--- a/examples/Coffee/dune
+++ b/examples/Coffee/dune
@@ -1,4 +1,4 @@
-(coq.theory
+(rocq.theory
  (name CTreeCoffee)
  (theories CTree)
 )
diff --git a/examples/ImpBr/ImpBr.v b/examples/ImpBr/ImpBr.v
index 9f590e9..3015b79 100755
--- a/examples/ImpBr/ImpBr.v
+++ b/examples/ImpBr/ImpBr.v
@@ -1,4 +1,3 @@
-Unset Universe Checking.
 
 From Stdlib Require Import
      Arith.PeanoNat
@@ -73,7 +72,8 @@ Variant MemE : Type -> Type :=
 
 Section Semantics.
 
-  Notation computation := (ctree MemE B2).
+  Universe computation_u.
+  Notation computation := (@ctree@{_ _ _ _ computation_u computation_u} MemE B2).
 
   Fixpoint denote_expr (e : expr) : computation value :=
     match e with
diff --git a/examples/ImpBr/dune b/examples/ImpBr/dune
index 1395468..49cad15 100755
--- a/examples/ImpBr/dune
+++ b/examples/ImpBr/dune
@@ -1,4 +1,4 @@
-(coq.theory
+(rocq.theory
   (name CTreeImp)
   (theories CTree)
 )
diff --git a/examples/SimpleSim/dune b/examples/SimpleSim/dune
index 881d647..aaa2f08 100644
--- a/examples/SimpleSim/dune
+++ b/examples/SimpleSim/dune
@@ -1,4 +1,4 @@
-(coq.theory
+(rocq.theory
  (name CTreeSimExample)
  (theories CTree)
 )
diff --git a/examples/Yield/Lang.v b/examples/Yield/Lang.v
index 6301837..8a32241 100644
--- a/examples/Yield/Lang.v
+++ b/examples/Yield/Lang.v
@@ -14,9 +14,6 @@ From ExtLib Require Import
      Data.List
      Data.Map.FMapAList.
 
-(* Universe issue, TO FIX *)
-Unset Universe Checking.
-Unset Auto Template Polymorphism.
 
 From ITree Require Import
      ITree
@@ -75,14 +72,19 @@ Variant MemE : Type -> Type :=
 | wr (x : var) (v : value) : MemE unit.
 
 Section Denote1.
+  Universes d q sd sq yd yq md mq.
   Definition is_true (v : value) : bool := if (v =? 0)%nat then false else true.
 
   Context (E := yieldE +' forkE +' MemE).
 
-  Definition while (step : ctree E void1 (unit + unit)) : ctree E void1 unit :=
+
+  Definition while
+      (step : @ctree@{_ _ _ _ d q} E void1 (unit + unit)) :
+      @ctree@{_ _ _ _ d q} E void1 unit :=
     CTree.iter (fun _ => step) tt.
 
-  Fixpoint denote_expr (e : expr) : ctree E void1 value :=
+  Fixpoint denote_expr (e : expr) :
+      @ctree@{_ _ _ _ d q} E void1 value :=
     match e with
     | Var v     => x <- trigger (rd v) ;; trigger Yield;; ret x
     | Lit n     => ret n
@@ -91,7 +93,8 @@ Section Denote1.
     | Mult a b  => l <- denote_expr a ;; r <- denote_expr b ;; ret (l * r)
     end.
 
-  Fixpoint denote_imp (s : stmt) : ctree E void1 unit :=
+  Fixpoint denote_imp (s : stmt) :
+      @ctree@{_ _ _ _ d q} E void1 unit :=
     match s with
     | Assign x e =>  v <- denote_expr e ;; u <- trigger (wr x v) ;; ret u
     | Seq a b    =>  denote_imp a ;; denote_imp b
@@ -118,40 +121,54 @@ Section Denote1.
   Definition interp_concurrency (t : stmt) : completed :=
     schedule 1 (fun _ => denote_imp t) (Some Fin.F1).
 
-  Definition handle_spawn : (yieldE +' spawnE +' MemE) ~> ctree (yieldE +' MemE) Bn :=
+  Definition handle_spawn : (yieldE +' spawnE +' MemE) ~>
+      @ctree@{_ _ _ _ sd sq} (yieldE +' MemE) Bn :=
     fun _ e =>
       match e with
       | inl1 y => trigger y
-      | inr1 (inl1 s) => match s with Spawn => ret tt end (* erase spawn events *)
+      | inr1 (inl1 s) => match s in spawnE T return
+          @ctree@{_ _ _ _ sd sq} (yieldE +' MemE) Bn T with Spawn => Ret tt end
       | inr1 (inr1 m) => trigger m
       end.
 
-  Definition interp_spawn : @completed MemE -> ctree (yieldE +' MemE) Bn unit :=
-    Fold.interp handle_spawn (T := unit).
-
-  Definition handle_yield : (yieldE +' MemE) ~> ctree MemE Bn :=
+  Definition interp_spawn : @completed MemE ->
+      @ctree@{_ _ _ _ sd sq} (yieldE +' MemE) Bn unit :=
+    Fold.interp handle_spawn (T:=unit).
+  Definition handle_yield : (yieldE +' MemE) ~>
+      @ctree@{_ _ _ _ yd yq} MemE Bn :=
     fun _ e =>
       match e with
-      | inl1 s => match s with Yield => ret tt end (* erase yield events *)
+      | inl1 s => match s in yieldE T return
+          @ctree@{_ _ _ _ yd yq} MemE Bn T with Yield => Ret tt end
       | inr1 m => trigger m
       end.
 
-  Definition interp_yield : ctree (yieldE +' MemE) Bn unit -> ctree MemE Bn unit :=
+  Definition interp_yield :
+      @ctree@{_ _ _ _ sd sq} (yieldE +' MemE) Bn unit ->
+      @ctree@{_ _ _ _ yd yq} MemE Bn unit :=
     Fold.interp handle_yield (T:=unit).
-
   (* list of key value pairs *)
   Definition env := alist var value.
-
-  Definition handle_state : MemE ~> Monads.stateT env (ctree void1 Bn) :=
+  Definition handle_state : MemE ~>
+      Monads.stateT env (@ctree@{_ _ _ _ md mq} void1 Bn) :=
     fun _ e s =>
       match e with
       | rd x => Ret (s, lookup_default x 0%nat s)
       | wr x v => Ret (Maps.add x v s, tt)
       end.
 
-  Definition interp_imp (t : stmt) : Monads.stateT env (ctree void1 Bn) unit :=
+
+  Definition interp_imp (t : stmt) :
+      Monads.stateT env (@ctree@{_ _ _ _ md mq} void1 Bn) unit :=
     interp_state handle_state (interp_yield (interp_spawn (interp_concurrency t))).
 
+  #[local] Arguments CTree.trigger : simpl never.
+  #[local] Arguments CTree.branch : simpl never.
+  #[local] Arguments CTree.bind : simpl never.
+  #[local] Arguments Fold.interp : simpl never.
+  #[local] Arguments interp_state : simpl never.
+  #[local] Arguments MonadBr_ctree : simpl never.
+
   Lemma schedule_forks_equ t1 t2 :
     (schedule 1 (fun _ : fin 1 => denote_imp (Fork t1 (Fork t2 Skip))) (Some Fin.F1))
       ≅
@@ -163,26 +180,41 @@ Section Denote1.
                         (fun _ => denote_imp t1))
                      None)).
   Proof.
+    cbn. repeat setoid_rewrite bind_trigger.
     rewrite rewrite_schedule. simp schedule_match.
     cbn. CTree.fold_subst.
-    unfold trigger.
     step. cbn. constructor. intros [].
+    rewrite (bind_ret_l tt (fun _ => trigger Spawn;;
+      Guard (schedule 2 (cons_vec (denote_imp t2) (fun _ => denote_imp t1)) None))).
+    etransitivity.
+    { apply equ_schedule with
+        (y := cons_vec (denote_imp t1)
+          (fun _ => Vis (subevent _ Par.Fork) (fun b : bool => if b then denote_imp t2 else Ret tt))); intros i.
+      dependent destruction i.
+      - simp cons_vec. rewrite bind_ret_l; reflexivity.
+      - dependent destruction i; [| inv i].
+        simp cons_vec. unfold replace_vec. cbn.
+        rewrite bind_ret_l, bind_trigger; reflexivity. }
+    cbn.
+    rewrite bind_trigger.
 
     rewrite rewrite_schedule. simp schedule_match. simp cons_vec.
     unfold replace_vec. cbn.
     step. cbn. constructor. intros [].
 
-    rewrite rewrite_schedule. simp schedule_match. simp cons_vec. cbn.
+    rewrite rewrite_schedule. simp schedule_match. simp cons_vec.
+    cbn.
     step. cbn. constructor.
 
     apply equ_schedule. intro i.
     dependent destruction i.
     - simp remove_vec. simp cons_vec. CTree.fold_subst.
-      rewrite bind_ret_l. reflexivity.
+      rewrite ?bind_ret_l. reflexivity.
     - dependent destruction i; [| inv i].
       simp remove_vec. simp cons_vec.
-      unfold remove_front_vec. simp cons_vec. cbn. simp cons_vec.
-      rewrite bind_ret_l. reflexivity.
+      unfold remove_front_vec. simp cons_vec.
+      cbn. simp cons_vec.
+      rewrite ?bind_ret_l. reflexivity.
   Qed.
 
   Equations p : fin 2 -> fin 2 :=
@@ -279,25 +311,30 @@ Section Denote1.
     (trigger Yield;;
      br1 (interp_concurrency s)).
   Proof.
-    unfold interp_concurrency. cbn.
+    unfold interp_concurrency.
+    etransitivity.
+    { apply equ_schedule; intros i; cbn; apply bind_trigger. }
+    setoid_rewrite bind_trigger.
 
     rewrite rewrite_schedule. simp schedule_match.
-    cbn. unfold trigger.
+    cbn.
     rewrite replace_vec_unary.
     step. cbn. constructor. intros [].
 
     rewrite rewrite_schedule. simp schedule_match.
-    CTree.fold_subst. rewrite (bind_ret_l tt).
-    simp cons_vec. cbn. rewrite remove_vec_cons_2.
+    CTree.fold_subst.
+    simp cons_vec. cbn.
+    rewrite remove_vec_cons_2.
     step. cbn. constructor.
 
     rewrite rewrite_schedule. simp schedule_match.
+    rewrite bind_trigger.
     step. cbn. constructor. intros [].
 
-    CTree.fold_subst. rewrite (bind_ret_l tt).
+    CTree.fold_subst.
     step. constructor; intros i.
     dependent destruction i. 2: inv i.
-    apply equ_schedule. repeat intro. rewrite bind_ret_l. reflexivity.
+    apply equ_schedule. repeat intro. reflexivity.
   Qed.
 
   Lemma yield_equ s :
@@ -306,7 +343,10 @@ Section Denote1.
     (trigger Yield;;
      br1 (interp_concurrency s)).
   Proof.
-    unfold interp_concurrency. cbn.
+    unfold interp_concurrency.
+    etransitivity.
+    { apply equ_schedule; intros i; cbn; apply bind_trigger. }
+    setoid_rewrite bind_trigger.
 
     rewrite rewrite_schedule. simp schedule_match.
     cbn. CTree.fold_subst.
@@ -321,7 +361,7 @@ Section Denote1.
     CTree.fold_subst.
     step. cbn. constructor; intros i.
     dependent destruction i. 2: inv i.
-    apply equ_schedule. repeat intro. rewrite bind_ret_l. reflexivity.
+    apply equ_schedule. repeat intro. rewrite ?bind_ret_l. reflexivity.
   Qed.
 
   Lemma br1_guard {F X} (t : ctree F Bn X) :
@@ -354,6 +394,8 @@ Section Denote1.
     reflexivity.
   Qed.
 
+
+
   Lemma fork_skip_yield s :
     interp_spawn (interp_concurrency (Seq YieldS s)) ~
     interp_spawn (interp_concurrency (Fork s Skip)).
@@ -388,14 +430,15 @@ Section Denote1.
     rewrite bind_ret_l. apply sb_guard.
   Qed.
 
+
   Lemma commut_forks_unfold s :
     interp_concurrency (Fork (While (Lit 1%nat) YieldS) (Fork s Skip)) ~
     interp_concurrency (Fork s (Fork (Seq YieldS (While (Lit 1%nat) YieldS)) Skip)).
   Proof.
     unfold interp_concurrency.
     do 2 rewrite schedule_forks_equ.
-    upto_bind_eq; intros [].
-    upto_bind_eq; intros [].
+    repeat setoid_rewrite bind_trigger.
+    do 2 (apply sb_vis; intros []).
     apply sb_guard_lr.
 
     apply schedule_order''.
@@ -405,9 +448,12 @@ Section Denote1.
 
   Lemma assign_equ :
     interp_concurrency (Assign "x" (Lit 2)) ≅
-                       (vis (wr "x" 2) (fun _ => Guard (ret tt))).
+      (vis (wr "x" 2) (fun _ => Guard (ret tt)) : @completed MemE).
   Proof.
-    unfold interp_concurrency. cbn.
+    unfold interp_concurrency.
+    etransitivity.
+    { apply equ_schedule with (y := fun _ => Vis (subevent _ (wr "x" 2)) (fun x => Ret x));
+        intros i; cbn; rewrite bind_ret_l, bind_trigger; reflexivity. }
 
     rewrite rewrite_schedule. simp schedule_match.
     cbn. CTree.fold_subst.
@@ -416,15 +462,22 @@ Section Denote1.
     rewrite rewrite_schedule. simp schedule_match.
     cbn. step. constructor.
 
-    rewrite rewrite_schedule. simp schedule_match. reflexivity.
+    rewrite rewrite_schedule. simp schedule_match.
+    step; cbn; constructor; reflexivity.
   Qed.
 
   Lemma fork_assign_assign_equ :
     interp_concurrency (Fork (Assign "x" (Lit 2))
                              (Assign "x" (Lit 1%nat))) ≅
-                       trigger Spawn;; (vis (wr "x" 1%nat) (fun _ => (Guard (trigger Yield;; br1 ((vis (wr "x" 2) (fun _ => Guard (ret tt)))))))).
+    (trigger Spawn;;
+      vis (wr "x" 1%nat) (fun _ => Guard
+        (trigger Yield;; br1 (vis (wr "x" 2) (fun _ => Guard (Ret tt)))))
+      : @completed MemE).
   Proof.
-    unfold interp_concurrency. cbn.
+    unfold interp_concurrency.
+    etransitivity.
+    { apply equ_schedule; intros i; cbn; apply bind_trigger. }
+    rewrite bind_trigger.
 
     rewrite rewrite_schedule. simp schedule_match.
     cbn. CTree.fold_subst.
@@ -441,15 +494,19 @@ Section Denote1.
     step. constructor.
 
     rewrite rewrite_schedule. simp schedule_match.
-    step. cbn. constructor. CTree.fold_subst. intros [].
+    step. cbn.
+    rewrite bind_trigger.
+    constructor. CTree.fold_subst. intros [].
     step. cbn. constructor. intros i.
 
     dependent destruction i. 2: inv i.
     rewrite remove_vec_cons_2.
-    rewrite rewrite_schedule. simp schedule_match. cbn.
+    rewrite rewrite_schedule. simp schedule_match.
+    cbn.
     step. constructor. intros [].
 
-    rewrite rewrite_schedule. simp schedule_match. cbn.
+    rewrite rewrite_schedule. simp schedule_match.
+    cbn.
     step. constructor.
 
     rewrite rewrite_schedule. simp schedule_match. reflexivity.
@@ -477,39 +534,32 @@ Section Denote1.
     interp_imp (Assign "x" (Lit 2)) s.
   Proof.
     unfold interp_imp.
-    rewrite fork_assign_assign_equ, assign_equ.
+    setoid_rewrite fork_assign_assign_equ.
+    setoid_rewrite assign_equ.
     unfold interp_yield, interp_spawn.
 
-    rewrite interp_bind. unfold trigger. rewrite interp_vis.
-    cbn. rewrite bind_ret_l. setoid_rewrite interp_ret.
-    rewrite ?interp_bind, ?interp_guard, ?bind_guard, interp_state_guard.
-    rewrite sb_guard.
-    rewrite interp_ret, bind_ret_l.
-
-    rewrite interp_vis; cbn.
-    unfold trigger; rewrite interp_vis; cbn.
-    rewrite bind_vis, interp_vis; cbn.
-    rewrite interp_state_bind, interp_state_trigger.
-    repeat (cbn; rewrite ?bind_bind, ?bind_ret_l, ?bind_guard, ?sb_guard, ?interp_guard, ?interp_state_guard).
-    unfold trigger. rewrite interp_bind, interp_vis; cbn.
-    rewrite bind_vis, interp_vis; cbn.
-    rewrite interp_state_bind, interp_state_trigger.
-    repeat (cbn; rewrite ?bind_bind, ?bind_ret_l, ?bind_guard, ?sb_guard, ?interp_guard, ?interp_state_guard).
-    unfold trigger. rewrite interp_bind, interp_vis; cbn.
-    repeat (cbn; rewrite ?bind_bind, ?bind_ret_l, ?bind_guard, ?sb_guard, ?interp_ret, ?interp_guard, ?interp_state_guard).
-    symmetry; rewrite ?sb_guard; symmetry.
-    rewrite ?interp_br', interp_state_br.
-    unfold branch; cbn. rewrite bind_br.
+    repeat (rewrite ?FoldCTree.interp_bind, ?FoldCTree.interp_trigger,
+      ?FoldCTree.interp_vis, ?FoldCTree.interp_guard, ?FoldCTree.interp_ret,
+      ?FoldCTree.interp_br', ?interp_state_bind, ?interp_state_trigger,
+      ?interp_state_vis, ?interp_state_guard, ?interp_state_ret,
+      ?bind_bind, ?bind_guard, ?bind_ret_l, ?subevent_subevent; cbn).
+    repeat apply sb_guard_l.
+    repeat apply sb_guard_r.
+    rewrite interp_state_br.
+    unfold mbr at 1; unfold MonadBr_ctree at 1.
+    cbn -[Fold.interp interp_state MonadBr_ctree].
+    rewrite bind_branch.
     apply sb_br_l; [exact Fin.F1 |].
-    intros ?.
-    repeat (cbn; rewrite ?bind_bind, ?bind_ret_l, ?bind_guard, ?sb_guard, ?interp_ret, ?interp_guard, ?interp_state_guard).
-    rewrite interp_vis; cbn.
-    unfold trigger; rewrite bind_vis, interp_vis; cbn.
-    rewrite interp_state_bind, interp_state_trigger.
-    repeat (cbn; rewrite ?bind_bind, ?bind_ret_l, ?bind_guard, ?sb_guard, ?interp_guard, ?interp_state_guard).
-    rewrite ?interp_ret, ?interp_state_ret.
+    intros i; dependent destruction i; [| now inversion i].
+    repeat (rewrite ?FoldCTree.interp_bind, ?FoldCTree.interp_trigger,
+      ?FoldCTree.interp_vis, ?FoldCTree.interp_guard, ?FoldCTree.interp_ret,
+      ?FoldCTree.interp_br', ?interp_state_bind, ?interp_state_trigger,
+      ?interp_state_vis, ?interp_state_guard, ?interp_state_ret,
+      ?bind_bind, ?bind_guard, ?bind_ret_l, ?subevent_subevent; cbn).
+    repeat apply sb_guard_l.
     apply sb_ret.
-    rewrite alist_add_alist_add. 2: apply RelDec_Correct_string. reflexivity.
+    rewrite alist_add_alist_add; [reflexivity | apply RelDec_Correct_string].
   Qed.
 
+
 End Denote1.
diff --git a/examples/Yield/Par.v b/examples/Yield/Par.v
index 15f6152..5b6a997 100644
--- a/examples/Yield/Par.v
+++ b/examples/Yield/Par.v
@@ -21,9 +21,6 @@ From RelationAlgebra Require Import
 
 From Equations Require Import Equations.
 
-(* Universe issue, TO FIX *)
-Unset Universe Checking.
-Unset Auto Template Polymorphism.
 
 From ITree Require Import
      State.
@@ -50,10 +47,13 @@ Variant spawnE : Type -> Type :=
   | Spawn : spawnE unit.
 
 Section parallel.
+  Universes e q q'.
   Context {E : Type -> Type}.
 
-  Definition thread := ctree (yieldE +' forkE +' E) void1 unit.
-  Definition completed := ctree (yieldE +' spawnE +' E) Bn unit.
+  Definition thread :=
+    @ctree@{e _ _ _ e q} (yieldE +' forkE +' E) void1 unit.
+  Definition completed :=
+    @ctree@{e _ _ _ e q'} (yieldE +' spawnE +' E) Bn unit.
   Definition vec n := fin n -> thread.
 
   (** Scheduling a thread pool *)
@@ -160,7 +160,8 @@ Section parallel.
 
   (*** how the scheduler behaves affects a thread *)
   (** inverting the case when a [schedule] is a [Br] *)
-  Lemma Br_schedule_inv n1 (e : Bn (fin n1)) k n2 (v : vec n2) i :
+  Polymorphic Lemma Br_schedule_inv n1 (e : Bn (fin n1))
+      (k : fin n1 -> completed) n2 (v : vec n2) i :
     Br e k ≅ schedule n2 v (Some i) -> False.
   (*   (exists k', v i ≅ Br e k' /\ *)
   (*            forall i', k i' ≅ schedule n2 (replace_vec v i (k' i')) (Some i)). *)
@@ -174,7 +175,7 @@ Section parallel.
     destruct c.
   Qed.
 
-  Lemma guard_schedule_inv t n (v : vec (S n)) (i : fin (S n)) :
+  Polymorphic Lemma guard_schedule_inv (t : completed) n (v : vec (S n)) (i : fin (S n)) :
     Guard t ≅ schedule _ v (Some i) ->
     (exists  t', v i ≅ Guard t' /\
              t ≅ schedule (S n) (replace_vec v i t') (Some i)) \/
@@ -190,7 +191,7 @@ Section parallel.
     - right; right.
       destruct r.
       split; auto.
-      step; rewrite Heqc; reflexivity.
+      step; rewrite Heqc; constructor; reflexivity.
     - left; eexists; split; eauto.
       step; rewrite Heqc; reflexivity.
     - destruct e; [destruct y | destruct s]; inv_equ.
@@ -203,7 +204,7 @@ Section parallel.
   Qed.
 
   (** Helper lemmas for when [schedule] transitions with a [val] *)
-  Lemma trans_schedule_val_1 {X} n v i (x : X) t :
+  Polymorphic Lemma trans_schedule_val_1 {X} n v i (x : X) t :
     trans (val x) (schedule n v (Some i)) t ->
     n = 1%nat.
   Proof.
@@ -239,7 +240,7 @@ Section parallel.
       destruct c.
   Qed.
 
-  Lemma trans_schedule_thread_val {X} v i (x : X) t :
+  Polymorphic Lemma trans_schedule_thread_val {X} v i (x : X) t :
     trans (val x) (schedule 1 v (Some i)) t ->
     trans (val x) (v i) Stuck.
   Proof.
@@ -267,9 +268,9 @@ Section parallel.
       + destruct Hequ as [EQ EQ'].
         rewrite EQ' in H. rewrite rewrite_schedule in H.
         simp schedule_match in H.
-        apply trans_ret_inv in H. destruct H. inv H0. invert.
-        rewrite EQ.
-        cbn.
+        dependent destruction H.
+        unfold trans, transR; cbn.
+        step in EQ; inv EQ.
         constructor.
     - invert.
       rewrite rewrite_schedule in Hequ.
@@ -296,7 +297,7 @@ Section parallel.
       invert. destruct n'; inv_equ.
       rewrite <- ctree_eta in Hequ.
       rewrite rewrite_schedule in Hequ. simp schedule_match in Hequ.
-      step in Hequ. inv Hequ. invert. exists n'.
+      step in Hequ. inv Hequ. repeat invert. exists n'.
       rewrite ctree_eta. rewrite <- Heq. rewrite <- H. rewrite REL. split; auto.
     }
     - destruct n'; inv_equ.
@@ -328,7 +329,8 @@ Section parallel.
       - destruct e; [destruct y | destruct s; [destruct f |]].
           try solve [step in Hequ; inv Hequ].
         rewrite <- ctree_eta in Hequ. step in Hequ; inv Hequ. invert.
-        rewrite <- ctree_eta in Hequ. step in Hequ; inv Hequ. invert.
+        all: repeat invert.
+        step in Hequ; inv Hequ; invert.
       - destruct c.
     }
     {
@@ -372,7 +374,7 @@ Section parallel.
       apply trans_schedule_obs_yield_None in H.
       destruct H as (?n' & ? & ?). subst.
       eexists. split.
-      + rewrite Hvi. constructor.
+      + unfold transR; cbn. step in Hvi; inv Hvi; constructor.
       + exists eq_refl. auto.
   Qed.
 
@@ -382,9 +384,10 @@ Section parallel.
     False.
   Proof.
     intros Ht.
-    unfold trans in Ht. cbn in Ht. red in Ht.
-    rewrite rewrite_schedule in *. destruct n; inv Ht. invert.
-    destruct (observe (schedule_match schedule (S n) v None)) eqn:?; invert.
+    unfold trans, transR in Ht; cbn in Ht.
+    rewrite rewrite_schedule in Ht.
+    destruct n; [inv Ht; invert |].
+    simp schedule_match in Ht; inv Ht; invert.
   Qed.
 
   (** [schedule] transitions with an [obs] of a [Spawn] *)
@@ -526,7 +529,7 @@ Section parallel.
   (*** how a thread [trans] affects the scheduler [trans] *)
 
   (** thread transitions with a val *)
-  Lemma trans_thread_schedule_val_1 {X} v i (x : X) t :
+  Polymorphic Lemma trans_thread_schedule_val_1 {X} v i (x : X) t :
     trans (val x) (v i) t ->
     trans (val x) (schedule 1 v (Some i)) Stuck.
   Proof.
@@ -628,6 +631,7 @@ Section parallel.
       rewrite rewrite_schedule at 1. simp schedule_match.
       econstructor. step. constructor. intros. apply equ_schedule.
       apply replace_vec_relation; repeat intro; auto.
+    all: invert; apply H.
   Qed.
 
   (** when the thread is a fork *)
@@ -649,7 +653,7 @@ Section parallel.
       rewrite <- Heqc. constructor.
       rewrite <- (replace_vec_twice _ v i t (k false)).
       eapply IHvisible_; auto; rewrite replace_vec_eq; eauto.
-    - invert.
+    - repeat invert.
       rewrite rewrite_schedule at 1. simp schedule_match.
       rewrite <- Heqc. econstructor. apply equ_schedule.
       apply cons_vec_relation; auto.
@@ -679,7 +683,7 @@ Section parallel.
   Qed.
 
   (*** Putting everything together *)
-  Lemma schedule_permutation n (v1 v2 : vec n) i (p q : fin n -> fin n)
+  Polymorphic Lemma schedule_permutation n (v1 v2 : vec n) i (p q : fin n -> fin n)
         (Hpq : forall i, p (q i) = i)
         (Hqp : forall i, q (p i) = i)
         (Hsb1 : forall i, v1 i ~ v2 (p i))
@@ -696,8 +700,8 @@ Section parallel.
     intros n v1 v2 i p q Hpq Hqp Hsb1 Hsb2 l t Ht. cbn in *.
     destruct l.
     - apply trans_schedule_thread_tau_some in Ht; auto.
-      assert (Hinjp : FinFun.Injective p) by (eapply bijective_injective; eauto).
-      assert (Hinjq : FinFun.Injective q) by (eapply bijective_injective; eauto).
+      assert (Hinjp : Finite.Injective p) by (eapply bijective_injective; eauto).
+      assert (Hinjq : Finite.Injective q) by (eapply bijective_injective; eauto).
       destruct n; try inv i.
       destruct Ht as (t' & Ht & Hequ).
       pose proof (Hsb1 i). step in H. destruct H as [Hf _].
@@ -719,11 +723,16 @@ Section parallel.
       + apply trans_schedule_obs_yield_Some in Ht; auto. destruct Ht.
         * (* The thread finished *)
           destruct H as (n' & Ht & (? & Hequ)); subst. cbn in *.
-          assert (Hinjp : FinFun.Injective p) by (eapply bijective_injective; eauto).
-          assert (Hinjq : FinFun.Injective q) by (eapply bijective_injective; eauto).
+          assert (Hinjp : Finite.Injective p) by (eapply bijective_injective; eauto).
+          assert (Hinjq : Finite.Injective q) by (eapply bijective_injective; eauto).
 
           epose proof (@remove_at_permutation_correct (yieldE +' forkE +' E) _ unit _ _ _ i Hpq Hqp Hinjp Hinjq) as (Hpq' & Hqp').
-          edestruct (@remove_at_permutation_vectors (yieldE +' forkE +' E) void1 unit n') as (Hpq'' & Hqp''); eauto.
+          pose proof
+            (@remove_at_permutation_vectors (yieldE +' forkE +' E) void1 unit n'
+              v1 v2 i p q Hinjp Hinjq
+              _ _
+              eq_refl eq_refl Hpq Hqp Hpq' Hqp' Hsb1 Hsb2)
+            as (Hpq'' & Hqp'').
           pose proof (Hsb1 i). step in H. destruct H as [Hf _].
           edestruct Hf as (? & ? & ? & ? & ?); eauto; subst.
           apply trans_thread_schedule_val_SS in H.
diff --git a/examples/Yield/Util.v b/examples/Yield/Util.v
index 40b22cd..de9a4ab 100644
--- a/examples/Yield/Util.v
+++ b/examples/Yield/Util.v
@@ -21,9 +21,6 @@ From RelationAlgebra Require Import
 
 From Equations Require Import Equations.
 
-(* Universe issue, TO FIX *)
-Unset Universe Checking.
-Unset Auto Template Polymorphism.
 
 From ITree Require Import
      State.
@@ -346,10 +343,11 @@ Section Vectors.
 
 End Vectors.
 
+Set Universe Polymorphism.
 Section Vector_brD_bound.
-  Context {E B : Type -> Type}.
-  Context {R : Type}.
-  Context (vec := fun n => fin n -> ctree E B R).
+  Universes r q.
+  Context {E : Type -> Type} {B : Type -> Type} {R : Type}.
+  Context (vec := fun n => fin n -> @ctree@{_ _ _ _ r q} E B R).
 
 (*   Lemma remove_front_vec_brD_bound n n' (v : vec (S n)) : *)
 (*     (forall i, brD_bound n' (v i)) -> *)
@@ -673,7 +671,7 @@ Section Vector_brD_bound.
 
   Definition remove_at_permutation {n} (p : fin (S (S n)) -> fin (S (S n)))
              (r : fin (S (S n)))
-             (Hp : FinFun.Injective p)
+             (Hp : Finite.Injective p)
     :
     { p' : (fin (S n) -> fin (S n)) &
              (forall i, match (order_cases i r) with
@@ -761,7 +759,7 @@ Section Vector_brD_bound.
 
   Lemma bijective_injective {n} (p q : fin n -> fin n)
         (Hqp: forall i, q (p i) = i) :
-    FinFun.Injective p.
+    Finite.Injective p.
   Proof.
     intros i1 i2 ?. apply (f_equal q) in H. do 2 rewrite Hqp in H. auto.
   Qed.
@@ -1110,3 +1108,4 @@ Section Vector_brD_bound.
     }
   Qed.
 End Vector_brD_bound.
+Unset Universe Polymorphism.
diff --git a/examples/Yield/dune b/examples/Yield/dune
index 9863f19..3aac469 100644
--- a/examples/Yield/dune
+++ b/examples/Yield/dune
@@ -1,4 +1,4 @@
-(coq.theory
+(rocq.theory
  (name CTreeYield)
- (theories CTree)
+ (theories CTree Equations)
 )
diff --git a/flake.lock b/flake.lock
index bbc2e75..5693948 100644
--- a/flake.lock
+++ b/flake.lock
@@ -3,15 +3,16 @@
     "coinduction-repo": {
       "flake": false,
       "locked": {
-        "lastModified": 1758090858,
-        "narHash": "sha256-S/stL5bpJsJt+bvOg4F2b/WaEt5IDOop3ruBIbde9GI=",
+        "lastModified": 1778079929,
+        "narHash": "sha256-ndGFgtFtqlfVpddyQDT9zSem218uJTqlLqI1wP38LSg=",
         "owner": "damien-pous",
         "repo": "coinduction",
-        "rev": "a88f0f4f170dcb9b24e3d470c76801a765423598",
+        "rev": "81ecd5f1ffa3e46b696d9461c88ad6ca9be5cfc7",
         "type": "github"
       },
       "original": {
         "owner": "damien-pous",
+        "ref": "v1.22",
         "repo": "coinduction",
         "type": "github"
       }
@@ -51,11 +52,11 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1762943920,
-        "narHash": "sha256-ITeH8GBpQTw9457ICZBddQEBjlXMmilML067q0e6vqY=",
+        "lastModified": 1791487292,
+        "narHash": "sha256-tqM7xDEsaeK1p6VvRygeZ9LkQRpUUkbRT02BHv6hnTM=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "91c9a64ce2a84e648d0cf9671274bb9c2fb9ba60",
+        "rev": "8edc0c72e3a38faf5434e40d1f19431125fe4b30",
         "type": "github"
       },
       "original": {
@@ -68,15 +69,16 @@
     "relation-algebra-repo": {
       "flake": false,
       "locked": {
-        "lastModified": 1758092026,
-        "narHash": "sha256-RnY+a57KnStACteaT5dKQoCCH0qp7/W+4qoaApIilj0=",
+        "lastModified": 1789980351,
+        "narHash": "sha256-SnSEdPajAcIgUzL0VKERXg6i+Lg2yJbNQYoJGNyfVYE=",
         "owner": "damien-pous",
         "repo": "relation-algebra",
-        "rev": "062d5cf9468ce367fe11220b336dff254a51702b",
+        "rev": "a6eb2b0dd62f0df2d198159176e5b28aa9643dae",
         "type": "github"
       },
       "original": {
         "owner": "damien-pous",
+        "ref": "v1.9.1",
         "repo": "relation-algebra",
         "type": "github"
       }
diff --git a/flake.nix b/flake.nix
index 01e8f94..a2906eb 100644
--- a/flake.nix
+++ b/flake.nix
@@ -6,11 +6,11 @@
     flake-utils.url = "github:numtide/flake-utils";
     nix-filter.url = "github:numtide/nix-filter";
     coinduction-repo = {
-      url = "github:damien-pous/coinduction";
+      url = "github:damien-pous/coinduction/v1.22";
       flake = false;
     };
     relation-algebra-repo = {
-      url = "github:damien-pous/relation-algebra";
+      url = "github:damien-pous/relation-algebra/v1.9.1";
       flake = false;
     };
   };
@@ -20,23 +20,23 @@
       let
         pkgs = import nixpkgs { inherit system; };
         lib = pkgs.lib;
-        rocq = pkgs.rocq-core;
-        rocqPkgs = pkgs.rocqPackages_9_0;
-        coqPkgs = pkgs.coqPackages_9_0;
+        rocqPkgs = pkgs.rocqPackages_9_2;
+        coqPkgs = pkgs.coqPackages_9_2;
+        rocq = rocqPkgs.rocq-core;
 
         coinduction = rocqPkgs.callPackage
           ( { rocq, stdenv }:
             rocqPkgs.mkRocqDerivation {
               owner = "damien-pous";
               pname = "coinduction";
-              version = "coinduction:master";
+              version = "1.22";
               src = coinduction-repo;
 
               buildInputs =
                 with rocqPkgs;
                 with coqPkgs;
                 with rocq.ocamlPackages;
-                [ ocaml camlp5 rocq pkgs.coq dune_3 stdlib rocq-core findlib ];
+                [ ocaml camlp5 rocq coqPkgs.coq dune_3 stdlib rocq-core findlib ];
               propagatedBuildInputs =
                 with rocqPkgs;
                 with coqPkgs;
@@ -49,14 +49,14 @@
             rocqPkgs.mkRocqDerivation {
               owner = "damien-pous";
               pname = "relation-algebra";
-              version = "relation-algebra:master";
+              version = "1.9.1";
               src = relation-algebra-repo;
 
               buildInputs =
                 with rocqPkgs;
                 with coqPkgs;
                 with rocq.ocamlPackages;
-                [ ocaml camlp5 rocq pkgs.coq dune_3 stdlib rocq-core findlib ];
+                [ ocaml camlp5 rocq coqPkgs.coq dune_3 stdlib rocq-core findlib ];
               propagatedBuildInputs =
                 with rocqPkgs;
                 with coqPkgs;
@@ -74,12 +74,13 @@
               opam-name = "rocq-ctree";
               useDune = true;
               src = ./.;
+              preBuild = "dune build rocq-ctree.opam && cp _build/default/rocq-ctree.opam .";
 
               buildInputs =
                 with rocqPkgs;
                 with coqPkgs;
                 with rocq.ocamlPackages;
-                [ ocaml camlp5 rocq pkgs.coq dune_3 ITree coinduction relation-algebra stdlib equations ExtLib zarith findlib ];
+                [ ocaml camlp5 rocq coqPkgs.coq dune_3 ITree coinduction relation-algebra stdlib equations ExtLib zarith findlib ];
               propagatedBuildInputs = [ rocq ];
 
             }) { inherit rocq; };
diff --git a/tests/ImpBrTest/ImpBrEx/ImpBrEx.v b/tests/ImpBrTest/ImpBrEx/ImpBrEx.v
index 790e61b..e89e9c7 100644
--- a/tests/ImpBrTest/ImpBrEx/ImpBrEx.v
+++ b/tests/ImpBrTest/ImpBrEx/ImpBrEx.v
@@ -1,4 +1,3 @@
-Unset Universe Checking.
 
 From Stdlib Require Import
      Strings.String.
diff --git a/tests/ImpBrTest/ImpBrEx/dune b/tests/ImpBrTest/ImpBrEx/dune
index 5e8dd5c..6f2617f 100644
--- a/tests/ImpBrTest/ImpBrEx/dune
+++ b/tests/ImpBrTest/ImpBrEx/dune
@@ -1,4 +1,4 @@
-(coq.theory
+(rocq.theory
  (name ImpBrEx)
  (theories CTree CTreeImp)
  )
diff --git a/tests/ImpBrTest/extracted/Extract.v b/tests/ImpBrTest/extracted/Extract.v
index bebcf27..266dc40 100644
--- a/tests/ImpBrTest/extracted/Extract.v
+++ b/tests/ImpBrTest/extracted/Extract.v
@@ -1,7 +1,6 @@
 Require Extraction.
 Require ExtrOcamlBasic.
 Require ExtrOcamlIntConv.
-Unset Universe Checking.
 Require ImpBrEx.ImpBrEx.
 
 Extraction Language OCaml.
diff --git a/tests/ImpBrTest/extracted/dune b/tests/ImpBrTest/extracted/dune
index 02c1561..f9c45e8 100644
--- a/tests/ImpBrTest/extracted/dune
+++ b/tests/ImpBrTest/extracted/dune
@@ -2,9 +2,9 @@
   (name extracted)
   (wrapped false)
   )
-(coq.extraction
+(rocq.extraction
   (prelude Extract)
-  (theories CTree CTreeImp ImpBrEx)
+  (theories Stdlib ExtLib Paco ITree Coinduction RelationAlgebra CTree CTreeImp ImpBrEx)
   (extracted_modules
     Applicative
     Ascii
diff --git a/tests/UniverseCheck/UniverseCheck.v b/tests/UniverseCheck/UniverseCheck.v
new file mode 100644
index 0000000..2bb2434
--- /dev/null
+++ b/tests/UniverseCheck/UniverseCheck.v
@@ -0,0 +1,54 @@
+From CTree Require Import Core.Utils Core.CTreeDefinitions Eq.Equ Eq.Trans
+  Interp.FoldCTree Interp.FoldStateT Interp.Recursion Interp.ITree.
+From ITree Require Import ITree InterpFacts Events.StateFacts.
+From RelationAlgebra Require Import rel srel.
+Import CTreeNotations EquNotations.
+Local Open Scope ctree_scope.
+Set Universe Checking.
+Set Universe Polymorphism.
+
+Section IndependentBudgets.
+  Universes i ri qi ro qo.
+  Constraint i < ri.
+  Constraint ri < qi.
+  Constraint qi < ro.
+  Constraint ro < qo.
+  Context (E : Type@{i} -> Type) (B : Type@{i} -> Type).
+  Context (X : Type@{i}) (ev : E X) (choice : B X).
+
+  Definition raised_trigger : @ctree@{i i _ _ ri qi} E B X := CTree.trigger ev.
+  Definition raised_branch : @ctree@{i i _ _ ri qi} E B X := CTree.branch choice.
+  Definition raised_branchS : @ctree@{i i _ _ ri qi} E B X := CTree.branchS choice.
+  Definition raised_monadic_trigger : @ctree@{i i _ _ ri qi} E B X :=
+    @Utils.mtrigger E (@ctree@{i i _ _ ri qi} E B) _ X ev.
+  Definition raised_monadic_branch : @ctree@{i i _ _ ri qi} E B X :=
+    @Utils.mbr B (@ctree@{i i _ _ ri qi} E B) _ X choice.
+  Definition continuation (x : X) : @ctree@{i i _ _ ro qo} E B X :=
+    CTreeDefinitions.Ret x.
+
+  Example bind_across_budgets :
+    CTree.bind raised_trigger continuation ≅ CTreeDefinitions.Vis ev continuation.
+  Proof. apply Equ.bind_trigger. Qed.
+
+  Example algebra_across_budgets
+      (t u : @ctree@{i i _ _ ri qi} E B X)
+      (v w : @ctree@{i i _ _ ro qo} E B X) :
+    (trans τ t u -> etrans τ t u) /\ (trans τ v w -> etrans τ v w).
+  Proof. split; apply trans_etrans. Qed.
+End IndependentBudgets.
+
+Section EventBelowBranch.
+  Universes e b.
+  Constraint e < b.
+  Context (E : Type@{e} -> Type) (B : Type@{b} -> Type).
+  Context (X : Type@{e}) (ev : E X).
+  Definition trigger_distinct_indices : ctree E B X := CTree.trigger ev.
+End EventBelowBranch.
+
+Section BranchBelowEvent.
+  Universes e b.
+  Constraint b < e.
+  Context (E : Type@{e} -> Type) (B : Type@{b} -> Type).
+  Context (X : Type@{b}) (choice : B X).
+  Definition branch_distinct_indices : ctree E B X := CTree.branch choice.
+End BranchBelowEvent.
diff --git a/tests/UniverseCheck/dune b/tests/UniverseCheck/dune
new file mode 100644
index 0000000..7842be8
--- /dev/null
+++ b/tests/UniverseCheck/dune
@@ -0,0 +1,3 @@
+(rocq.theory
+ (name CTreeUniverseCheck)
+ (theories CTree ITree RelationAlgebra))
diff --git a/theories/Core/CTreeDefinitions.v b/theories/Core/CTreeDefinitions.v
index f1fb5f4..b4f6da0 100644
--- a/theories/Core/CTreeDefinitions.v
+++ b/theories/Core/CTreeDefinitions.v
@@ -35,6 +35,7 @@ From ExtLib Require Import
 Set Implicit Arguments.
 Set Contextual Implicit.
 Set Primitive Projections.
+Set Universe Polymorphism.
 
 (*|
 .. coq::
@@ -42,7 +43,8 @@ Set Primitive Projections.
 
 Section ctree.
 
-  Context {E : Type -> Type} {B : Type -> Type} {R : Type}.
+  Universe e b.
+  Context {E : Type@{e} -> Type} {B : Type@{b} -> Type} {R : Type}.
 
 (*|
 The type [ctree] is defined as the final coalgebra ("greatest fixed point") of the functor [ctreeF].
@@ -60,8 +62,8 @@ value returned by the environment
     | StuckF
     | StepF  (t : ctree)
     | GuardF (t : ctree)
-    | VisF {X : Type} (e : E X) (k : X -> ctree)           (* an external event *)
-    | BrF {X : Type} (c : B X) (k : X -> ctree)            (* an internal non-deterministic branching *)
+    | VisF {X : Type@{e}} (e : E X) (k : X -> ctree)      (* an external event *)
+    | BrF {X : Type@{b}} (c : B X) (k : X -> ctree)       (* an internal non-deterministic branching *)
   .
 
   CoInductive ctree : Type :=
@@ -258,22 +260,29 @@ Functorial map ([fmap] in Haskell)
     Definition map {R S} (f : R -> S)  (t : ctree E B R) : ctree E B S :=
       bind t (fun x => Ret (f x)).
 
+
+
+  End CTree.
+
+  Section AtomicTrees.
+    Universes d q.
+    Context {E : Type -> Type} {B : Type -> Type}.
 (*|
 Atomic itrees triggering a single event.
 |*)
 
-    Definition trigger : E ~> ctree E B :=
-      fun R e => Vis e (fun x => Ret x).
+    Definition trigger : E ~> @ctree@{_ _ _ _ d q} E B :=
+      fun T e => Vis e (fun x => Ret x).
 
 (*|
 Atomic ctrees with choice.
 |*)
 
-    Definition branch {X : Type} : forall (c : B X), ctree E B X :=
-      fun c => Br c (fun x => Ret x).
+    Definition branch {X : Type} (c : B X) : @ctree@{_ _ _ _ d q} E B X :=
+      Br c (fun x => Ret x).
 
-    Definition branchS {X : Type} : forall (c : B X), ctree E B X :=
-      fun c => BrS c (fun x => Ret x).
+    Definition branchS {X : Type} (c : B X) : @ctree@{_ _ _ _ d q} E B X :=
+      BrS c (fun x => Ret x).
 
 (*|
 Ignore the result of a tree.
@@ -282,7 +291,8 @@ Ignore the result of a tree.
     Definition ignore {R} : ctree E B R -> ctree E B unit :=
       map (fun _ => tt).
 
-  End CTree.
+  End AtomicTrees.
+  Arguments trigger {E B} [T] _.
 
   Ltac fold_bind :=
     repeat match goal with
@@ -403,18 +413,22 @@ Instances
 #[global] Instance MonadIter_ctree {E B} : MonadIter (ctree E B) :=
   fun R I => @CTree.iter E B R I.
 
-#[global] Instance MonadTrigger_ctree {E F B} `{E -< F} : MonadTrigger E (ctree F B) :=
+#[global] Instance MonadTrigger_ctree@{d q +} {E : Type -> Type} {F : Type -> Type} {B}
+  `{E -< F} : MonadTrigger E (@ctree@{_ _ _ _ d q} F B) :=
   fun _ e => trigger e.
 
-#[global] Instance MonadBr_ctree {E C D} `{C -< D} : MonadBr C (ctree E D) :=
+#[global] Instance MonadBr_ctree@{d q +} {E} {C : Type -> Type} {D : Type -> Type}
+  `{C -< D} : MonadBr C (@ctree@{_ _ _ _ d q} E D) :=
   fun _ c => branch c.
 
 #[global] Instance MonadStuck_ctree {E C} : MonadStuck (ctree E C) :=
   fun _ => Stuck.
 
-#[global] Instance MonadStep_ctree {E C} : MonadStep (ctree E C) :=
+#[global] Instance MonadStep_ctree@{d q +} {E C} :
+  MonadStep (@ctree@{_ _ _ _ d q} E C) :=
   Step (Ret tt).
 
+
 (*|
 ====================================
 Inversion lemma relying on [JMeq_eq]
diff --git a/theories/Core/Utils.v b/theories/Core/Utils.v
index 43101d3..571960b 100644
--- a/theories/Core/Utils.v
+++ b/theories/Core/Utils.v
@@ -7,11 +7,13 @@ From ITree Require Import Basics.Basics.
 
 Notation fin := Fin.t.
 
-Polymorphic Class MonadTrigger (E : Type -> Type) (M : Type -> Type) : Type :=
-  mtrigger : forall {X}, E X -> M X.
+Polymorphic Class MonadTrigger@{ei +}
+  (E : Type@{ei} -> Type) (M : Type -> Type) : Type :=
+  mtrigger : forall {X : Type@{ei} }, E X -> M X.
 
-Polymorphic Class MonadBr (B : Type -> Type) (M : Type -> Type) : Type :=
-  mbr : forall {X}, B X -> M X.
+Polymorphic Class MonadBr@{bi +}
+  (B : Type@{bi} -> Type) (M : Type -> Type) : Type :=
+  mbr : forall {X : Type@{bi} }, B X -> M X.
 
 Polymorphic Class MonadStep (M : Type -> Type) : Type :=
   mstep : M unit.
diff --git a/theories/Eq/Epsilon.v b/theories/Eq/Epsilon.v
index 476d0fa..4586cb4 100644
--- a/theories/Eq/Epsilon.v
+++ b/theories/Eq/Epsilon.v
@@ -10,6 +10,7 @@ From CTree Require Import
 
 Import CTreeNotations.
 Open Scope ctree_scope.
+Set Universe Polymorphism.
 
 (* end hide *)
 
diff --git a/theories/Eq/Equ.v b/theories/Eq/Equ.v
index c751531..f538d35 100644
--- a/theories/Eq/Equ.v
+++ b/theories/Eq/Equ.v
@@ -25,6 +25,7 @@ From CTree Require Import
      Eq.Shallow.
 
 Import CTree.
+Set Universe Polymorphism.
 
 #[local] Ltac step_ := step; simpl body.
 #[local] Ltac step := step_.
@@ -265,13 +266,12 @@ Proof.
     cbn.
     rewrite <- x in EQu.
     dependent destruction EQu.
-    rewrite <- x. eauto.
+    rewrite <- x. constructor; eauto.
   - dependent destruction EQ.
     cbn.
     rewrite <- x in EQu.
     dependent destruction EQu.
-    rewrite <- x.
-    eauto.
+    rewrite <- x. constructor; eauto.
 Qed.
 
 #[global] Instance equb_eq_equ {E B X} {Q : rel X X} :
@@ -692,7 +692,7 @@ Sufficient condition to prove compatibility only over the simulation
 Lemma equ_clos_sym {E C X} : compat converse (@equ_clos E E C C X X).
 Proof.
   intros R t u EQ; inv EQ.
-  apply Equ_clos with u' t'; intuition.
+  apply Equ_clos with u' t'; intuition; symmetry; assumption.
 Qed.
 
 Lemma equ_clos_equ {E C X L} {c: Chain (fequ L)}:
@@ -713,10 +713,10 @@ Proof.
     inv Equu; constructor; apply IH; econstructor; eauto.
     dependent induction H1; dependent induction H2. inv Equu.
     dependent induction H2; dependent induction H3.
-    econstructor; intros. apply IH; econstructor; eauto.
+    econstructor; intros. apply IH; econstructor; [apply REL | apply REL0 | apply REL1].
     dependent induction H1; dependent induction H2. inv Equu.
     dependent induction H2; dependent induction H3.
-    econstructor; intros. apply IH; econstructor; eauto.
+    econstructor; intros. apply IH; econstructor; [apply REL | apply REL0 | apply REL1].
 Qed.
 
 #[global] Instance equ_eq_equ_goal_gen {E C R L} (r : Chain (@fequ E C R R L)) :
@@ -885,13 +885,30 @@ Proof.
   now rewrite unfold_bind.
 Qed.
 
-Lemma bind_trigger {E B X Y} (e : E X) (k : X -> ctree E B Y) :
-  trigger e >>= k ≅ Vis e k.
+Section AtomicEquations.
+  Universes d q d' q'.
+  Context {E : Type -> Type} {B : Type -> Type}.
+
+Lemma unfold_branch {X} (c : B X) :
+  (CTree.branch c : @ctree@{_ _ _ _ d q} E B X) = Br c (fun x => Ret x).
+Proof. reflexivity. Qed.
+
+
+Lemma unfold_trigger {X} (e : E X) :
+  (CTree.trigger e : @ctree@{_ _ _ _ d q} E B X) = Vis e (fun x => Ret x).
+Proof. reflexivity. Qed.
+
+Lemma bind_trigger {X Y}
+    (e : E X) (k : X -> @ctree@{_ _ _ _ d' q'} E B Y) :
+  (CTree.trigger e : @ctree@{_ _ _ _ d q} E B X) >>= k ≅ Vis e k.
 Proof.
-  unfold trigger; rewrite bind_vis; setoid_rewrite bind_ret_l.
+  rewrite unfold_trigger, bind_vis; setoid_rewrite bind_ret_l.
   reflexivity.
 Qed.
 
+End AtomicEquations.
+
+
 Lemma bind_stuck {E B X Y} (g : X -> ctree E B Y):
   Stuck >>= g ≅ Stuck.
 Proof.
@@ -916,13 +933,22 @@ Proof.
   now rewrite unfold_bind.
 Qed.
 
-Lemma bind_branch : forall {E C X Y} (c : C Y) (k : Y -> ctree E C X),
-    branch c >>= k ≅ Br c k.
+Section BranchBindEquations.
+  Universes d q d' q'.
+  Context {E : Type -> Type} {C : Type -> Type}.
+
+Lemma bind_branch {X Y}
+    (c : C Y) (k : Y -> @ctree@{_ _ _ _ d' q'} E C X) :
+  (CTree.branch c : @ctree@{_ _ _ _ d q} E C Y) >>= k ≅ Br c k.
 Proof.
-  intros. rewrite unfold_bind. cbn. setoid_rewrite bind_ret_l.
+  rewrite unfold_branch, bind_br; setoid_rewrite bind_ret_l.
   reflexivity.
 Qed.
 
+
+End BranchBindEquations.
+
+
 Tactic Notation "sinv" ident(H) := step in H; inv H.
 
 Lemma stuck_equ_bind {E B X Y} :
diff --git a/theories/Eq/IterFacts.v b/theories/Eq/IterFacts.v
index 67f53a3..7e7eabe 100644
--- a/theories/Eq/IterFacts.v
+++ b/theories/Eq/IterFacts.v
@@ -15,6 +15,7 @@ From CTree Require Import
 
 Import CTree.
 Import CTreeNotations.
+Set Universe Polymorphism.
 
 Definition iter_gen {E B X I}
     (step : I -> ctree E B (I + X)) (t : ctree E B (I + X)) :=
diff --git a/theories/Eq/SBisim.v b/theories/Eq/SBisim.v
index 9665d34..fc367d2 100644
--- a/theories/Eq/SBisim.v
+++ b/theories/Eq/SBisim.v
@@ -66,6 +66,7 @@ From RelationAlgebra Require Export
 
 Import CoindNotations.
 Set Implicit Arguments.
+Set Universe Polymorphism.
 Import CTree.
 Import CTreeNotations.
 Import EquNotations.
@@ -625,12 +626,17 @@ Lemma vis_chain_gen {E F C D: Type -> Type} {X X' Y Y': Type} L
 Proof.
   intros.
   apply (b_chain R).
-  split; intros ?? TR; inv_trans; subst.
-  do 2 eexists; intuition; eauto.
-  rewrite EQ; auto.
-  do 2 eexists; intuition; eauto.
-  rewrite EQ; apply H2.
-  apply H0.
+  split; intros ? ? TR; inv_trans; subst.
+  - exists (obs e' (right x)), (k' (right x)); repeat split.
+    + apply trans_vis.
+    + eapply equ_clos_sb_ctx;
+        [symmetry; exact EQ | reflexivity | exact (H1 x)].
+    + exact (H x).
+  - exists (obs e (left x)), (k (left x)); repeat split.
+    + apply trans_vis.
+    + eapply equ_clos_sb_ctx;
+        [reflexivity | symmetry; exact EQ | exact (H2 x)].
+    + exact (H0 x).
 Qed.
 
 Lemma vis_chain {E C X Y}
@@ -1309,8 +1315,11 @@ produce any challenge for the other.
       @spin_gen E C Z X c ~ @spin_gen E C Z Y c'.
   Proof.
     intros R.
-    coinduction S _; split; cbn;
-      intros * TR; exfalso; eapply spinD_gen_is_stuck, TR.
+    coinduction S _; split; cbn.
+    - intros * TR; exfalso.
+      now apply spinD_gen_is_stuck in TR.
+    - intros * TR; exfalso.
+      now apply spinD_gen_is_stuck in TR.
   Qed.
 
 (*|
@@ -1371,13 +1380,14 @@ produce any challenge for the other.
   Lemma br2_spin_l {X} : forall (t : ctree E C X),
 	    br2 spin t ~ t.
   Proof.
-    intros; apply br2_is_stuck, spin_is_stuck.
+    intros; apply br2_is_stuck.
+    red; intros l u TR; now apply spin_is_stuck in TR.
   Qed.
 
   Lemma br2_spin_r {X} : forall (t : ctree E C X),
 	    br2 t spin ~ t.
   Proof.
-    intros; rewrite br2_commut; apply br2_is_stuck, spin_is_stuck.
+    intros; rewrite br2_commut; apply br2_spin_l.
   Qed.
 
 (*|
@@ -1539,6 +1549,7 @@ Not fond of this, need to give some thoughts about them
       do 2 eexists; intuition; eauto.
       apply trans_val_inv in TR0.
       rewrite TR0; eauto.
+    all: apply trans_ret.
   Qed.
 
 End WithParams.
@@ -1689,9 +1700,10 @@ Section StrongSimulations.
         rewrite EQ; auto.
       - step; intros ?? TR.
         inv_trans; subst.
-        exists τ, (Ret tt); intuition; now rewrite EQ.
-        exists τ, (Ret tt). intuition.
-        rewrite EQ; apply Stuck_ssim.
+        exists τ, (Ret tt); split; [apply trans_step |].
+        split; [now rewrite EQ | reflexivity].
+        exists τ, (Ret tt); split; [apply trans_step |].
+        split; [rewrite EQ; apply Stuck_ssim | reflexivity].
       - step in H. cbn in H. destruct H as [_ ?].
         specialize (H τ Stuck). lapply H; [| etrans].
         intros. destruct H0 as (? & ? & ? & ? & ?).
diff --git a/theories/Eq/SBisimAlt.v b/theories/Eq/SBisimAlt.v
index 363a253..7f9226e 100644
--- a/theories/Eq/SBisimAlt.v
+++ b/theories/Eq/SBisimAlt.v
@@ -24,6 +24,7 @@ From RelationAlgebra Require Export
 Import CoindNotations.
 Import CTree.
 Set Implicit Arguments.
+Set Universe Polymorphism.
 
 (* TODO: Decide where to set this *)
 Arguments trans : simpl never.
diff --git a/theories/Eq/SSim.v b/theories/Eq/SSim.v
index 289a129..6c9d39e 100644
--- a/theories/Eq/SSim.v
+++ b/theories/Eq/SSim.v
@@ -23,6 +23,7 @@ From RelationAlgebra Require Export
 Import CoindNotations.
 Import CTree.
 Set Implicit Arguments.
+Set Universe Polymorphism.
 
 (* TODO: Decide where to set this *)
 Arguments trans : simpl never.
@@ -651,11 +652,13 @@ Section Proof_Rules.
     intros.
     cbn; intros ? ? TR; inv_trans; subst;
       destruct (H0 x) as (x' & RR & LL);
-      cbn; eexists; eexists; intuition.
-    - rewrite EQ; eauto.
-    - assumption.
+      cbn; exists (obs f x'), (k' x'); repeat split.
+    - apply trans_vis.
+    - eapply H; [symmetry; exact EQ | reflexivity | exact RR].
+    - exact LL.
   Qed.
 
+
   Lemma step_ss_vis {Y Z Z' F D} (e : E Z) (f: F Z')
         (k : Z -> ctree E C X) (k' : Z' -> ctree F D Y) (L : rel _ _)
     {R : Chain (@ss E F C D X Y L)} :
diff --git a/theories/Eq/SSimAlt.v b/theories/Eq/SSimAlt.v
index 43c7edb..97335b4 100644
--- a/theories/Eq/SSimAlt.v
+++ b/theories/Eq/SSimAlt.v
@@ -22,6 +22,7 @@ From RelationAlgebra Require Export
 Import CoindNotations.
 Import CTree.
 Set Implicit Arguments.
+Set Universe Polymorphism.
 
 (* TODO: Decide where to set this *)
 Arguments trans : simpl never.
@@ -335,9 +336,10 @@ Section Proof_Rules.
     intros. split; [| split]; intros; inv_equ.
     cbn; inv_trans; subst;
       destruct (H x) as (x' & RR & LL);
-      cbn; do 3 eexists; intuition.
-    - rewrite EQ; eauto.
-    - assumption.
+      cbn; exists (obs f x'), (k' x'); repeat split.
+    - apply trans_vis.
+    - eapply HR; [symmetry; exact EQ | reflexivity | exact RR].
+    - exact LL.
   Qed.
 
   Lemma step_ss'_vis_id {Z} (e : E Z) (f: F Z)
@@ -498,6 +500,7 @@ Section Proof_Rules.
     split; [| split]; intros; inv_equ.
     inv_trans; subst.
     cbn; do 3 eexists; intuition; subs; eauto.
+    all: apply trans_step.
   Qed.
 
   Lemma step_ss'_step_l :
diff --git a/theories/Eq/Shallow.v b/theories/Eq/Shallow.v
index 362dacc..b47fd83 100644
--- a/theories/Eq/Shallow.v
+++ b/theories/Eq/Shallow.v
@@ -26,6 +26,7 @@ From Stdlib Require Import
      JMeq.
 
 Set Implicit Arguments.
+Set Universe Polymorphism.
 (* end hide *)
 
 Definition eqeq {A : Type} (P : A -> Type) {a1 a2 : A} (p : a1 = a2) : P a1 -> P a2 -> Prop :=
diff --git a/theories/Eq/Trace.v b/theories/Eq/Trace.v
index d2e9342..a0ad256 100644
--- a/theories/Eq/Trace.v
+++ b/theories/Eq/Trace.v
@@ -9,6 +9,8 @@ From CTree Require Import
   Eq.Trans
   Eq.SSim
   Eq.SBisim.
+Set Universe Polymorphism.
+
 
 (*|
 Base coinductive definitions for execution traces and trace equivalence.
diff --git a/theories/Eq/Trans.v b/theories/Eq/Trans.v
index 910860e..f2bae7d 100644
--- a/theories/Eq/Trans.v
+++ b/theories/Eq/Trans.v
@@ -61,6 +61,7 @@ Open Scope ctree.
 
 Set Implicit Arguments.
 Set Primitive Projections.
+Set Universe Polymorphism.
 
 #[local] Tactic Notation "step" := __step_equ.
 #[local] Tactic Notation "step" "in" ident(H) := __step_in_equ H.
@@ -71,7 +72,10 @@ Set Primitive Projections.
 
 Section Trans.
 
-  Context {E B : Type -> Type} {R : Type}.
+  Universes e b v.
+  Context {E : Type@{e} -> Type}.
+  Context {B : Type@{b} -> Type}.
+  Context {R : Type}.
 
   Notation S' := (ctree' E B R).
   Notation S  := (ctree  E B R).
@@ -88,11 +92,11 @@ least annoying solution.
 |*)
   Variant label : Type :=
     | τ
-    | obs {X : Type} (e : E X) (v : X)
-    | val {X : Type} (v : X).
+    | obs {X : Type@{e} } (e : E X) (v : X)
+    | val {X : Type@{v} } (v : X).
 
   Variant is_val : label -> Prop :=
-    | Is_val : forall X (x : X), is_val (val x).
+    | Is_val : forall (X : Type@{v}) (x : X), is_val (val x).
 
   Lemma is_val_τ : ~ is_val τ.
   Proof.
@@ -115,7 +119,7 @@ node, labelling the transition by the returned value.
 |*)
   Inductive trans_ : label -> hrel S' S' :=
 
-  | Transbr {X} (c : B X) x k l t :
+  | Transbr {X : Type@{b} } (c : B X) x k l t :
     trans_ l (observe (k x)) t ->
     trans_ l (BrF c k) t
 
@@ -127,7 +131,7 @@ node, labelling the transition by the returned value.
     u ≅ t ->
     trans_ τ (StepF t) (observe u)
 
-  | Transobs {X} (e : E X) k x t :
+  | Transobs {X : Type@{e} } (e : E X) k x t :
     k x ≅ t ->
     trans_ (obs e x) (VisF e k) (observe t)
 
@@ -847,8 +851,9 @@ Lemma etrans_ret_inv {E B X} : forall x l (t : ctree E B X),
     (l = τ /\ t ≅ Ret x) \/ (l = val x /\ t ≅ Stuck).
 Proof.
   intros ? [] ? step; cbn in step.
-  - intuition; try (eapply trans_ret in step; now apply step).
-    inv H.
+  - destruct step as [step | step].
+    + apply trans_ret_inv in step as [_ abs]. inv abs.
+    + left; split; [reflexivity | now symmetry].
   - eapply trans_ret_inv in step; intuition.
   - eapply trans_ret_inv in step; intuition.
 Qed.
@@ -1018,7 +1023,7 @@ Section wtrans.
     rewrite EQ in step3; apply trans_τ_str_ret_inv in step3; auto.
     rewrite EQ in step3.
     apply transs_is_stuck_inv in step3; [| apply Stuck_is_stuck].
-    intuition.
+    right; split; [reflexivity | now symmetry].
   Qed.
 
   Lemma wtrans_val_inv' : forall (x : X) (t v : ctree E B X),
@@ -1494,41 +1499,34 @@ Proof.
     eapply wtrans_bind_r'; eauto.
 Qed.
 
-Lemma trans_trigger : forall {E B X Y} (e : E X) x (k : X -> ctree E B Y),
-    trans (obs e x) (trigger e >>= k) (k x).
+Section TriggerTransitions.
+  Universes d q d' q'.
+  Context {E : Type -> Type} {B : Type -> Type}.
+
+Lemma trans_trigger {X Y} (e : E X) x (k : X -> @ctree@{_ _ _ _ d' q'} E B Y) :
+  trans (obs e x) ((CTree.trigger e : @ctree@{_ _ _ _ d q} E B X) >>= k) (k x).
 Proof.
-  intros.
-  unfold CTree.trigger.
-  rewrite unfold_bind; cbn.
-  setoid_rewrite bind_ret_l.
-  constructor; auto.
+  rewrite bind_trigger; apply trans_vis.
 Qed.
 
-Lemma trans_trigger' : forall {E B X Y} (e : E X) x (t : ctree E B Y),
-    trans (obs e x) (trigger e;; t) t.
+Lemma trans_trigger' {X Y} (e : E X) x (t : @ctree@{_ _ _ _ d' q'} E B Y) :
+  trans (obs e x) ((CTree.trigger e : @ctree@{_ _ _ _ d q} E B X);; t) t.
 Proof.
-  intros.
-  unfold CTree.trigger.
-  rewrite unfold_bind; cbn.
-  setoid_rewrite bind_ret_l.
-  constructor; auto.
+  rewrite bind_trigger; apply trans_vis.
 Qed.
 
-Lemma trans_trigger_inv : forall {E B X Y} (e : E X) (k : X -> ctree E B Y) l u,
-    trans l (trigger e >>= k) u ->
-    exists x, u ≅ k x /\ l = obs e x.
+Lemma trans_trigger_inv {X Y} (e : E X) (k : X -> @ctree@{_ _ _ _ d' q'} E B Y)
+    l (u : @ctree@{_ _ _ _ d' q'} E B Y) :
+  trans l ((CTree.trigger e : @ctree@{_ _ _ _ d q} E B X) >>= k) u ->
+  exists x, u ≅ k x /\ l = obs e x.
 Proof.
-  intros * TR.
-  unfold trigger in TR.
-  apply trans_bind_inv in TR.
-  destruct TR as [(? & ? & TR & ?) |(? & TR & ?)].
-  - apply trans_vis_inv in TR.
-    destruct TR as (? & ? & ->); eexists; split; eauto.
-    rewrite H0, H1, bind_ret_l; reflexivity.
-  - apply trans_vis_inv in TR.
-    destruct TR as (? & ? & abs); inv abs.
+  intros TR.
+  rewrite bind_trigger in TR; apply trans_vis_inv in TR.
+  exact TR.
 Qed.
 
+End TriggerTransitions.
+
 Lemma trans_branch :
   forall {E B : Type -> Type} {X : Type} {Y : Type}
     [l : label] [t t' : ctree E B X] (c : B Y) (k : Y -> ctree E B X) (x : Y),
diff --git a/theories/Eq/Visible.v b/theories/Eq/Visible.v
index 0a4f526..c654bc0 100644
--- a/theories/Eq/Visible.v
+++ b/theories/Eq/Visible.v
@@ -21,6 +21,7 @@ Open Scope ctree.
 
 Set Implicit Arguments.
 Set Primitive Projections.
+Set Universe Polymorphism.
 
 #[local] Tactic Notation "step" "in" ident(H) := __step_in_equ H.
 
diff --git a/theories/Eq/WBisim.v b/theories/Eq/WBisim.v
index e423271..1ee732c 100644
--- a/theories/Eq/WBisim.v
+++ b/theories/Eq/WBisim.v
@@ -377,24 +377,24 @@ on the setoid side.
       unfold wtrans, etrans. ka.
     Qed.
 
-    Lemma cnv_wt (R : Chain wb) : (elem R: hrel _ _)° ≡ elem R.
+    Lemma cnv_wt (R : Chain wb) : (elem R: hrel _ _)^° ≡ elem R.
     Proof. apply RelationAlgebra.lattice.antisym; intros ???; apply sym_t,H. Qed.
-    Lemma cnv_gfp: RelationAlgebra.lattice.weq ((gfp wb: hrel _ _)°) (gfp wb).
+    Lemma cnv_gfp: RelationAlgebra.lattice.weq ((gfp wb: hrel _ _)^°) (gfp wb).
     Proof. apply cnv_wt. Qed.
-    Lemma cnv_wbisim: wbisimT° ≡ wbisimT.
+    Lemma cnv_wbisim: wbisimT^° ≡ wbisimT.
     Proof. apply cnv_wt. Qed.
-    Lemma cnv_wbisim': wbisim° ≡ wbisim.
+    Lemma cnv_wbisim': wbisim^° ≡ wbisim.
     Proof. apply cnv_wt. Qed.
 
 
 (*|
 By symmetry, similar results for left-to-right game
 |*)
-    Lemma wbisim_trans_front l: (trans l)° ⋅ wbisimT ≦ wbisimT ⋅ (wtrans l)°.
+    Lemma wbisim_trans_front l: (trans l)^° ⋅ wbisimT ≦ wbisimT ⋅ (wtrans l)^°.
     Proof. cnv_switch. rewrite 2cnvdot, cnv_invol, cnv_wbisim. apply wbisim_trans_back. Qed.
-    Lemma wbisim_etrans_front l: (etrans l)° ⋅ wbisimT ≦ wbisimT ⋅ (wtrans l)°.
+    Lemma wbisim_etrans_front l: (etrans l)^° ⋅ wbisimT ≦ wbisimT ⋅ (wtrans l)^°.
     Proof. cnv_switch. rewrite 2cnvdot, cnv_invol, cnv_wbisim. apply wbisim_etrans_back. Qed.
-    Lemma wbisim_wtrans_front l: (wtrans l)° ⋅ wbisimT ≦ wbisimT ⋅ (wtrans l)°.
+    Lemma wbisim_wtrans_front l: (wtrans l)^° ⋅ wbisimT ≦ wbisimT ⋅ (wtrans l)^°.
     Proof. cnv_switch. rewrite 2cnvdot, cnv_invol, cnv_wbisim. apply wbisim_wtrans_back. Qed.
 
 (*|
diff --git a/theories/Interp/Fold.v b/theories/Interp/Fold.v
index d7c6cd0..48ebfa6 100644
--- a/theories/Interp/Fold.v
+++ b/theories/Interp/Fold.v
@@ -13,6 +13,7 @@ From CTree Require Import
      CTree Eq.
 
 Set Implicit Arguments.
+Set Universe Polymorphism.
 
 Import CTreeNotations.
 Open Scope ctree_scope.
@@ -26,7 +27,7 @@ Open Scope ctree_scope.
     - a local scheduler [B ~> M] describing valid branches
     and defines for it a monad morphism [ctree E B ~> M]
     for any monad [M] with a loop operator. *)
-Definition fold {E B M : Type -> Type}
+Definition fold {E : Type -> Type} {B : Type -> Type} {M : Type -> Type}
            {FM : Functor M} {MM : Monad M} {IM : MonadIter M}
            {Mstuck : MonadStuck M} {Mstep : MonadStep M}
            (h : E ~> M)
@@ -54,7 +55,7 @@ Arguments fold {E B M FM MM IM Mstuck Mstep} h g [T].
     and re-emit external events (internalized in [M] via [MonadTrigger]
  *)
 
-Definition interp {E B M : Type -> Type}
+Definition interp {E : Type -> Type} {B : Type -> Type} {M : Type -> Type}
   {FM : Functor M} {MM : Monad M}
   {IM : MonadIter M}
   {Mstuck : MonadStuck M}
@@ -65,12 +66,11 @@ Definition interp {E B M : Type -> Type}
 
 Arguments interp {E B M FM MM IM _ _ _} h [T].
 
-Definition refine {E B M : Type -> Type}
+Definition refine {E : Type -> Type} {B : Type -> Type} {M : Type -> Type}
   {FM : Functor M} {MM : Monad M} {IM : MonadIter M} {TM : MonadTrigger E M}
   {Mstuck : MonadStuck M}
   {Mstep : MonadStep M}
-  (g : B ~> M)
-  :=
+  (g : B ~> M) : ctree E B ~> M :=
   fold (fun _ e => mtrigger e) g.
 
 Arguments refine {E B M FM MM IM TM _ _} g [T].
@@ -122,7 +122,7 @@ Proof.
     apply CH. apply REL.
 Qed.
 
-#[global] Instance refine_equ {E C D X} (h : C ~> ctree E D):
+#[global] Instance refine_equ {E C D X} h:
   Proper (equ eq ==> @equ E D X X eq) (@refine E C _ _ _ _ _ _ _ h X).
 Proof.
   cbn.
diff --git a/theories/Interp/FoldCTree.v b/theories/Interp/FoldCTree.v
index 7515189..6068dc3 100644
--- a/theories/Interp/FoldCTree.v
+++ b/theories/Interp/FoldCTree.v
@@ -1,5 +1,4 @@
 (* begin hide *)
-Unset Universe Checking.
 
 From ExtLib Require Import
      Structures.Functor
@@ -18,6 +17,8 @@ From CTree Require Import
   Misc.Pure
   Fold.
 
+Set Universe Polymorphism.
+
 Import CTreeNotations.
 Open Scope ctree_scope.
 
@@ -34,12 +35,17 @@ Section FoldCTree.
   Section With_Params.
 
     (** Specialization to [M = ctree F (B01 +' D)] *)
-    Context {E F C D: Type -> Type} {X : Type}
-      {h : E ~> ctree F D} {g : C ~> ctree F D}.
+    Universes d q d' q'.
+    Context {E : Type -> Type} {F : Type -> Type}
+      {C : Type -> Type} {D : Type -> Type} {X : Type}
+      {h : E ~> @ctree@{_ _ _ _ d' q'} F D}
+      {g : C ~> @ctree@{_ _ _ _ d' q'} F D}.
+
 
     (** ** [interpE] and constructors *)
-    Definition fold_ctree : forall [T], ctree E C T -> ctree F D T :=
-      fold h g.
+    Definition fold_ctree :
+      @ctree@{_ _ _ _ d q} E C ~> @ctree@{_ _ _ _ d' q'} F D := fold h g.
+    Arguments fold_ctree [T] _.
       (* fold (mstuck (M := ctree F D)) (mstep (M := ctree F D)) h (mbr (M := ctree F D)) g. *)
       (* fold (fun T => Stuck: ctree F D T) (Step (Ret tt)) h g. *)
 
@@ -55,7 +61,7 @@ Section FoldCTree.
        end)%function.
 
     (** Unfold lemma. *)
-    Lemma unfold_fold_ctree (t: ctree E C X):
+    Lemma unfold_fold_ctree (t : ctree E C X):
       fold_ctree t ≅ fold_ctree_ t.
     Proof.
       unfold fold_ctree, fold, Basics.iter, MonadIter_ctree, mbr, MonadBr_ctree, CTree.branch.
@@ -73,7 +79,7 @@ Section FoldCTree.
     Qed.
 
     Lemma fold_ctree_ret (x: X):
-      fold_ctree (Ret x) ≅ Ret x.
+      fold_ctree (Ret x : ctree E C X) ≅ (Ret x : @ctree@{_ _ _ _ d' q'} F D X).
     Proof. now rewrite unfold_fold_ctree. Qed.
 
     Lemma fold_ctree_vis {U} (e: E U) (k: U -> ctree E C X) :
@@ -81,7 +87,7 @@ Section FoldCTree.
     Proof. now rewrite unfold_fold_ctree. Qed.
 
     Lemma fold_ctree_stuck :
-      fold_ctree (Stuck : ctree E C X) ≅ Stuck.
+      fold_ctree (Stuck : ctree E C X) ≅ (Stuck : @ctree@{_ _ _ _ d' q'} F D X).
     Proof. now rewrite unfold_fold_ctree. Qed.
 
     Lemma fold_ctree_guard (t : ctree E C X) :
@@ -92,7 +98,7 @@ Section FoldCTree.
       fold_ctree (Step t) ≅ Step (Guard (fold_ctree t)).
     Proof. now rewrite unfold_fold_ctree. Qed.
 
-    Lemma fold_ctree_br {U} (c : C U) (k: _ -> ctree E C X) :
+    Lemma fold_ctree_br {U} (c : C U) (k: U -> ctree E C X) :
       fold_ctree (Br c k) ≅ x <- g _ c;; Guard (fold_ctree (k x)).
     Proof. now rewrite unfold_fold_ctree. Qed.
 
@@ -113,6 +119,7 @@ Section FoldCTree.
         intros ?; constructor; auto.
     Qed.
 
+
     (** Unfolding of [interp]. *)
 
     Notation interp_ h t :=
@@ -126,7 +133,7 @@ Section FoldCTree.
        end)%function.
 
     (** Unfold lemma. *)
-    Lemma unfold_interp `{C -< D} (t: ctree E C X):
+    Lemma unfold_interp `{C -< D} (t : @ctree@{_ _ _ _ d q} E C X):
       interp h t ≅ interp_ h t.
     Proof.
       unfold interp,fold, Basics.iter, MonadIter_ctree, mbr, MonadBr_ctree, CTree.branch.
@@ -143,7 +150,8 @@ Section FoldCTree.
     Qed.
 
     Lemma interp_ret `{C -< D} (x: X):
-      interp h (Ret x : ctree E C X) ≅ Ret x.
+      interp h (Ret x : @ctree@{_ _ _ _ d q} E C X) ≅
+      (Ret x : @ctree@{_ _ _ _ d' q'} F D X).
     Proof. now rewrite unfold_interp. Qed.
 
     Lemma interp_stuck `{C -< D} :
@@ -163,13 +171,14 @@ Section FoldCTree.
     Proof. now rewrite unfold_interp. Qed.
 
     Lemma interp_br `{C -< D} {U} (c : C U) (k: _ -> ctree E C X) :
-      interp h (Br c k) ≅ x <- branch c;; Guard (interp h (k x)).
+      interp h (Br c k) ≅ x <- mbr c;; Guard (interp h (k x)).
     Proof. now rewrite unfold_interp. Qed.
 
     Lemma interp_br' `{C -< D} {U} (c : C U) (k: _ -> ctree E C X) :
-      interp h (Br c k) ≅ br c (fun x => Guard (interp h (k x))).
-    Proof. rewrite interp_br; unfold branch; rewrite bind_br; setoid_rewrite bind_ret_l.
-           reflexivity.
+      interp h (Br c k) ≅
+      br c (fun x => Guard (interp h (k x))).
+    Proof. rewrite interp_br. unfold mbr, MonadBr_ctree.
+           rewrite bind_branch; reflexivity.
     Qed.
 
     #[global] Instance interp_equ `{C -< D} {R} :
@@ -179,7 +188,7 @@ Section FoldCTree.
       coinduction r CIH.
       intros * EQ; step in EQ.
       rewrite 2 unfold_interp.
-      inv EQ.
+      inv EQ; rewrite <- H1, <- H2.
       - constructor; auto.
       - constructor; auto.
       - constructor; auto.
@@ -202,7 +211,7 @@ Section FoldCTree.
        end)%function.
 
     (** Unfold lemma. *)
-    Lemma unfold_refine `{E -< F} (t: ctree E C X):
+    Lemma unfold_refine `{E -< F} (t : @ctree@{_ _ _ _ d q} E C X):
       refine g t ≅ refine_ g t.
     Proof.
       unfold refine,fold, Basics.iter, MonadIter_ctree, mbr, MonadBr_ctree, CTree.branch.
@@ -219,27 +228,28 @@ Section FoldCTree.
     Qed.
 
     Lemma refine_ret `{E -< F} (x: X):
-      refine g (Ret x : ctree E C X) ≅ Ret x.
+      refine g (Ret x : @ctree@{_ _ _ _ d q} E C X) ≅ Ret x.
     Proof. now rewrite unfold_refine. Qed.
 
     Lemma refine_vis `{E -< F} {U} (e: E U) (k: U -> ctree E C X) :
-      refine g (Vis e k) ≅ x <- trigger e;; Guard (refine g (k x)).
+      refine g (Vis e k) ≅ x <- mtrigger e;; Guard (refine g (k x)).
     Proof. now rewrite unfold_refine. Qed.
 
     Lemma refine_trigger `{E -< F} (e: E X) :
-        refine g (trigger e : ctree E C X) ~ (trigger e : ctree F D X).
+        refine g (trigger e : @ctree@{_ _ _ _ d q} E C X) ~
+          (mtrigger e : @ctree@{_ _ _ _ d' q'} F D X).
     Proof.
-      rewrite unfold_refine; cbn.
+      rewrite Equ.unfold_trigger, unfold_refine; cbn.
       setoid_rewrite sb_guard.
-      setoid_rewrite refine_ret.
+      setoid_rewrite unfold_refine; cbn.
       now rewrite bind_ret_r.
     Qed.
 
-    Lemma refine_guard `{E -< F} (t: ctree E C X) :
+    Lemma refine_guard `{E -< F} (t : @ctree@{_ _ _ _ d q} E C X) :
       refine g (Guard t) ≅ Guard (refine g t).
     Proof. now rewrite unfold_refine. Qed.
 
-    Lemma refine_step `{E -< F} (t: ctree E C X) :
+    Lemma refine_step `{E -< F} (t : @ctree@{_ _ _ _ d q} E C X) :
       refine g (Step t) ≅ Step (Guard (refine g t)).
     Proof. now rewrite unfold_refine. Qed.
 
@@ -254,7 +264,7 @@ Section FoldCTree.
       coinduction r CIH.
       intros * EQ; step in EQ.
       rewrite 2 unfold_refine.
-      inv EQ; try constructor; auto.
+      inv EQ; rewrite <- H1, <- H2; try constructor; auto.
       - step; constructor; auto.
       - upto_bind_eq.
         intros ?; constructor; auto.
@@ -264,13 +274,35 @@ Section FoldCTree.
 
   End With_Params.
 
+
+  Lemma interp_trigger@{d q d' q' +}
+      {E : Type -> Type} {F : Type -> Type} {C : Type -> Type} {D : Type -> Type}
+      {h : E ~> @ctree@{_ _ _ _ d' q'} F D} `{C -< D} {U : Type} (e : E U) :
+      interp h (CTree.trigger e : @ctree@{_ _ _ _ d q} E C U) ≅
+      (x <- h _ e;; Guard (Ret x) : @ctree@{_ _ _ _ d' q'} F D U).
+    Proof.
+      rewrite Equ.unfold_trigger, interp_vis;
+        setoid_rewrite interp_ret; reflexivity.
+    Qed.
+
+
+
+
+
+
   Arguments fold_ctree {E F C D} h g [T].
 
   Section FoldBind.
 
-    Context {E F C D: Type -> Type} {X : Type}.
+    Universes d0 q0 d q d' q'.
+    Context {E : Type -> Type} {F : Type -> Type}
+      {C : Type -> Type} {D : Type -> Type} {X : Type}.
 
-    Lemma fold_ctree_bind (h : E ~> ctree F D) (g : C ~> ctree F D) {S} (t : ctree E C X) (k : X -> ctree _ _ S) :
+    Lemma fold_ctree_bind
+      (h : E ~> @ctree@{_ _ _ _ d' q'} F D)
+      (g : C ~> @ctree@{_ _ _ _ d' q'} F D) {S : Type}
+      (t : @ctree@{_ _ _ _ d0 q0} E C X)
+      (k : X -> @ctree@{_ _ _ _ d q} E C S) :
       fold_ctree h g (t >>= k) ≅ fold_ctree h g t >>= (fun x => fold_ctree h g (k x)).
     Proof.
       revert t.
@@ -295,14 +327,22 @@ Section FoldCTree.
         now constructor.
     Qed.
 
-    Lemma interp_bind (h : E ~> ctree F D) `{C -< D} {S} (t : ctree E C X) (k : X -> ctree _ _ S) :
+    Lemma interp_bind
+      (h : E ~> @ctree@{_ _ _ _ d' q'} F D)
+      `{C -< D} {S : Type}
+      (t : @ctree@{_ _ _ _ d0 q0} E C X)
+      (k : X -> @ctree@{_ _ _ _ d q} E C S) :
       interp h (t >>= k) ≅ interp h t >>= (fun x => interp h (k x)).
     Proof.
       unfold interp.
       now setoid_rewrite fold_ctree_bind.
     Qed.
 
-    Lemma refine_bind (g : C ~> ctree F D) `{E -< F} {S} (t : ctree E C X) (k : X -> ctree _ _ S) :
+    Lemma refine_bind
+      (g : C ~> @ctree@{_ _ _ _ d' q'} F D)
+      `{E -< F} {S : Type}
+      (t : @ctree@{_ _ _ _ d0 q0} E C X)
+      (k : X -> @ctree@{_ _ _ _ d q} E C S) :
       refine g (t >>= k) ≅ refine g t >>= (fun x => refine g (k x)).
     Proof.
       unfold refine.
@@ -313,6 +353,7 @@ Section FoldCTree.
 
 End FoldCTree.
 
+
 (*|
 Counter-example showing that interp does not preserve sbisim in the general case.
 |*)
@@ -322,7 +363,6 @@ Module CounterExample.
   Inductive VoidE : Type -> Type :=
   | voidE : VoidE void.
 
-  (* Notation B012 := (B01 +' B2). *)
   #[local] Definition t1 := Ret 1 : ctree VoidE B2 nat.
   #[local] Definition t2 := br2 (Ret 1) (x <- trigger voidE;; match x : void with end) : ctree VoidE B2 nat.
 
@@ -331,22 +371,33 @@ Module CounterExample.
     unfold t1, t2.
     rewrite br2_commut.
     rewrite br2_is_stuck. reflexivity.
-    red. intros. intro. inv_trans.  destruct x.
+    red. intros. intro.
+    rewrite bind_trigger in H.
+    apply trans_vis_inv in H as (x & _ & _). destruct x.
   Qed.
 
-  #[local] Definition h : VoidE ~> ctree VoidE B2.
-  Proof.
-    intros. destruct X. exact (Step Stuck).
-  Defined.
+  Section Handler.
+    Universes d q.
+    #[local] Definition h : VoidE ~> @ctree@{_ _ _ _ d q} VoidE B2 :=
+      fun _ e => match e with voidE => Step Stuck end.
+
+
+    #[local] Definition interp_h :=
+      @interp VoidE B2 (@ctree@{_ _ _ _ d q} VoidE B2)
+        _ _ _ _ _ (@MonadBr_ctree VoidE B2 B2 _) h.
+  End Handler.
+  Arguments interp_h [T] _.
 
-  Example interpE_sbsisim_counterexample : ~ (interp h t1 ~ interp h t2).
+  Example interpE_sbsisim_counterexample : ~ (interp_h t1 ~ interp_h t2).
   Proof.
     red. intros. unfold t2 in H.
     playR in H.
+    unfold interp_h.
     rewrite unfold_interp. cbn. setoid_rewrite bind_br.
     eapply trans_br with (x := false).
     2: { rewrite bind_ret_l. reflexivity. }
     apply trans_guard. setoid_rewrite unfold_interp. cbn. rewrite bind_step. etrans.
+    unfold interp_h in TR.
     rewrite unfold_interp in TR. unfold t1, h in TR. cbn in TR. inv_trans.
   Qed.
 
@@ -354,8 +405,8 @@ End CounterExample.
 
 Section epsilon_interp_theory.
 
-  Lemma interp_productive {E C F X} (h : E ~> ctree F C) : forall (t : ctree E C X),
-      productive (interp h t) -> productive t.
+  Lemma interp_productive {E C F X} h : forall (t : ctree E C X),
+      productive (interp (M := ctree F C) h t) -> productive t.
   Proof.
     intros. inversion H;
       subst;
@@ -367,9 +418,9 @@ Section epsilon_interp_theory.
       try now econstructor.
   Qed.
 
-  Lemma epsilon_interp : forall {E C F X}
-                           (h : E ~> ctree F C) (t t' : ctree E C X),
-      epsilon t t' -> epsilon (interp h t) (interp h t').
+  Lemma epsilon_interp : forall {E C F X} h (t t' : ctree E C X),
+      epsilon t t' ->
+      epsilon (interp (M := ctree F C) h t) (interp h t').
   Proof.
     intros. red in H. setoid_rewrite (ctree_eta t). setoid_rewrite (ctree_eta t').
     genobs t ot. genobs t' ot'. clear t Heqot t' Heqot'.
@@ -384,9 +435,9 @@ Section epsilon_interp_theory.
 
 End epsilon_interp_theory.
 
-Lemma interp_ret_inv {E F B X} (h : E ~> ctree F B) :
+Lemma interp_ret_inv {E F B X} h :
   forall (t : ctree E B X) r,
-  interp h t ≅ Ret r -> t ≅ Ret r.
+  interp (M := ctree F B) h t ≅ Ret r -> t ≅ Ret r.
 Proof.
   intros. setoid_rewrite (ctree_eta t) in H. setoid_rewrite (ctree_eta t).
   destruct (observe t) eqn:?; try now inv_equ.
@@ -400,11 +451,10 @@ Proof.
   intros. rewrite bind_bind. upto_bind_eq; intros ?. rewrite bind_guard. setoid_rewrite bind_ret_l. reflexivity.
 Qed.
 
-Lemma trans_val_interp {E F B X}
-  (h : E ~> ctree F B) :
+Lemma trans_val_interp {E F B X} h :
   forall (t u : ctree E B X) (v : X),
   trans (val v) t u ->
-  trans (val v) (interp h t) Stuck.
+  trans (val v) (interp (M := ctree F B) h t) Stuck.
 Proof.
   intros.
   apply trans_val_epsilon in H as []. subs.
@@ -413,11 +463,10 @@ Proof.
   rewrite interp_ret. etrans.
 Qed.
 
-Lemma trans_tau_interp {E F B X}
-  (h : E ~> ctree F B) :
+Lemma trans_tau_interp {E F B X} h :
   forall (t u : ctree E B X),
   trans τ t u ->
-  trans τ (interp h t) (Guard (interp h u)).
+  trans τ (interp (M := ctree F B) h t) (Guard (interp h u)).
 Proof.
   intros.
   apply trans_τ_epsilon in H as (? & ? & ?). subs.
@@ -427,14 +476,13 @@ Proof.
   etrans.
 Qed.
 
-Lemma trans_obs_interp_step {E F B X Y}
-  (h : E ~> ctree F B) :
+Lemma trans_obs_interp_step {E F B X Y} h :
   forall (t u : ctree E B X) u' (e : E Y) x l,
   trans (obs e x) t u ->
   trans l (h _ e) u' ->
   ~ is_val l ->
   epsilon_det u' (Ret x) ->
-  trans l (interp h t) (u';; Guard (interp h u)).
+  trans l (interp (M := ctree F B) h t) (u';; Guard (interp h u)).
 Proof.
   intros.
   apply trans_obs_epsilon in H as (? & ? & ?).
@@ -447,12 +495,11 @@ Proof.
   apply trans_bind_l; auto.
 Qed.
 
-Lemma trans_obs_interp_pure {E F B X Y}
-  (h : E ~> ctree F B) :
+Lemma trans_obs_interp_pure {E F B X Y} h :
   forall (t u : ctree E B X) (e : E Y) x,
   trans (obs e x) t u ->
   trans (val x) (h _ e) Stuck ->
-  epsilon (interp h t) (Guard (interp h u)).
+  epsilon (interp (M := ctree F B) h t) (Guard (interp h u)).
 Proof.
   intros t u e x TR TRh.
   apply trans_obs_epsilon in TR as (k & EPS & ?). subs.
diff --git a/theories/Interp/FoldStateT.v b/theories/Interp/FoldStateT.v
index 18ce555..94f20d4 100644
--- a/theories/Interp/FoldStateT.v
+++ b/theories/Interp/FoldStateT.v
@@ -1,4 +1,3 @@
-Unset Universe Checking.
 
 From Stdlib Require Import Classes.RelationPairs.
 
@@ -23,13 +22,15 @@ From CTree Require Import
      Misc.Pure.
 
 Import SBisimNotations.
-Import MonadNotation.
-Open Scope monad_scope.
 
 Set Implicit Arguments.
+Set Universe Polymorphism.
 
 (* TODO MOVE *)
 Arguments fequ : simpl never.
+Section StateMonadOperations.
+Import MonadNotation.
+Open Scope monad_scope.
 
 #[global] Instance MonadBr_stateT {S M C} {MM : Monad M} {AM : MonadBr C M}:
   MonadBr C (stateT S M) :=
@@ -62,8 +63,11 @@ Definition refine_state {E C M} S
   ctree E C ~> stateT S M := refine g.
 
 #[global] Typeclasses Opaque fold_state interp_state refine_state.
+End StateMonadOperations.
 
 Section State.
+  Import CTreeNotations.
+  Universes d q d' q'.
   Variable (S : Type).
   Variant stateE : Type -> Type :=
     | Get : stateE S
@@ -72,25 +76,29 @@ Section State.
   Definition get {E C} `{stateE -< E} : ctree E C S := trigger Get.
   Definition put {E C} `{stateE -< E} : S -> ctree E C unit := fun s => trigger (Put s).
 
-  Definition h_state {E C} : stateE ~> stateT S (ctree E C) :=
+  Definition h_state {E C} : stateE ~> stateT S (@ctree@{_ _ _ _ d' q'} E C) :=
     fun _ e s =>
       match e with
       | Get => Ret (s, s)
       | Put s' => Ret (s', tt)
       end.
 
-  Definition pure_state {E C} : E ~> stateT S (ctree E C)
-    := fun _ e s => Vis e (fun x => Ret (s, x)).
+  Definition pure_state {E C} : E ~> stateT S (@ctree@{_ _ _ _ d' q'} E C) :=
+    fun _ e s => (x <- CTree.trigger e;; Ret (s, x))%ctree.
 
-  Definition pure_state_choice {E C} : C ~> stateT S (ctree E C)
-    := fun _ c s => br c (fun x => Ret (s, x)).
+  Definition pure_state_choice {E C} : C ~> stateT S (@ctree@{_ _ _ _ d' q'} E C) :=
+    fun _ c s => (x <- CTree.branch c;; Ret (s, x))%ctree.
 
-  Definition run_state {E C}
-    : ctree (stateE +' E) C ~> stateT S (ctree E C) :=
-    fold_state (case_ h_state pure_state) pure_state_choice.
+  Definition run_state {E C} :
+      @ctree@{_ _ _ _ d q} (stateE +' E) C ~>
+        stateT S (@ctree@{_ _ _ _ d' q'} E C) :=
+    fold_state (case_sum1 h_state pure_state) pure_state_choice.
 
 End State.
 
+Import MonadNotation.
+Open Scope monad_scope.
+
 Ltac break :=
   match goal with
   | v: _ * _ |- _ => destruct v
@@ -101,11 +109,13 @@ Ltac break :=
    [itree E ~> stateT S (itree F)]. *)
 Section State.
 
+  Universes d q d' q'.
+
   Variable (S : Type).
-  Context {E F C D : Type -> Type}
-          {R : Type}
-          (h : E ~> stateT S (ctree F D))
-          (g : C ~> stateT S (ctree F D)).
+  Context {E : Type -> Type} {F : Type -> Type}
+          {C : Type -> Type} {D : Type -> Type} {R : Type}
+          (h : E ~> stateT S (@ctree@{_ _ _ _ d' q'} F D))
+          (g : C ~> stateT S (@ctree@{_ _ _ _ d' q'} F D)).
 
   (** Unfolding of [fold]. *)
   Notation fold_state_ h g t s :=
@@ -118,7 +128,7 @@ Section State.
      | BrF c k => bind (g _ c s) (fun xs => Guard (fold_state h g (k (snd xs)) (fst xs)))
      end)%function.
 
-  Lemma unfold_fold_state (t : ctree E C R) (s : S) :
+  Lemma unfold_fold_state (t : @ctree@{_ _ _ _ d q} E C R) (s : S) :
     fold_state h g t s ≅ fold_state_ h g t s.
   Proof.
     unfold fold_state, fold, MonadIter_stateT0, iter, MonadIter_ctree, Basics.iter.
@@ -144,7 +154,7 @@ Section State.
 
   #[global] Instance equ_fold_state:
     Proper (equ eq ==> eq ==> equ eq)
-           (fold_state h g (T := R)).
+           (fold_state h g (T := R) : @ctree@{_ _ _ _ d q} E C R -> _).
   Proof.
     unfold Proper, respectful.
     coinduction r IH; intros * EQ1 * <-.
@@ -160,7 +170,8 @@ Section State.
 
   Lemma fold_state_ret
         (s : S) (r : R) :
-    (fold_state h g (Ret r) s) ≅ (Ret (s, r)).
+    fold_state h g (Ret r : @ctree@{_ _ _ _ d q} E C R) s ≅
+      (Ret (s, r) : @ctree@{_ _ _ _ d' q'} F D (S * R)).
   Proof.
     rewrite ctree_eta. reflexivity.
   Qed.
@@ -171,52 +182,53 @@ Section State.
     now rewrite ctree_eta.
   Qed.
 
-  Lemma fold_state_guard (t : ctree E C R) (s : S) :
+  Lemma fold_state_guard (t : @ctree@{_ _ _ _ d q} E C R) (s : S) :
     fold_state h g (Guard t) s ≅ Guard (fold_state h g t s).
   Proof.
     now rewrite unfold_fold_state; cbn.
   Qed.
 
-  Lemma fold_state_step (t : ctree E C R) (s : S) :
+  Lemma fold_state_step (t : @ctree@{_ _ _ _ d q} E C R) (s : S) :
     fold_state h g (Step t) s ≅ Step (Guard (fold_state h g t s)).
   Proof.
     now rewrite unfold_fold_state; cbn.
   Qed.
 
   Lemma fold_state_vis {T : Type}
-    (e : E T) (k : T -> ctree E C R) (s : S) :
-    fold_state h g (Vis e k) s ≅ h e s >>= fun sx => Guard (fold_state h g (k (snd sx)) (fst sx)).
+    (e : E T) (k : T -> @ctree@{_ _ _ _ d q} E C R) (s : S) :
+    fold_state h g (Vis e k) s ≅
+      h e s >>= fun sx => Guard (fold_state h g (k (snd sx)) (fst sx)).
   Proof.
     rewrite unfold_fold_state; reflexivity.
   Qed.
 
   Lemma fold_state_br {T: Type} `{C -< D}
-    (c : C T) (k : T -> ctree E C R) (s : S) :
-    fold_state h g (br c k) s ≅ g c s >>= fun sx => Guard (fold_state h g (k (snd sx)) (fst sx)).
+    (c : C T) (k : T -> @ctree@{_ _ _ _ d q} E C R) (s : S) :
+    fold_state h g (br c k) s ≅
+      g c s >>= fun sx => Guard (fold_state h g (k (snd sx)) (fst sx)).
   Proof.
     rewrite !unfold_fold_state; reflexivity.
   Qed.
 
   Lemma fold_state_trigger (e : E R) (s : S) :
-    fold_state h g (CTree.trigger e) s ≅
-    h e s >>= fun x => Guard (Ret x).
+    fold_state h g (CTree.trigger e : @ctree@{_ _ _ _ d q} E C R) s ≅
+    ((h e s >>= fun x => Guard (Ret x)) : @ctree@{_ _ _ _ d' q'} F D (S * R)).
   Proof.
-    unfold CTree.trigger.
-    rewrite fold_state_vis; cbn.
+    rewrite Equ.unfold_trigger, fold_state_vis; cbn.
     upto_bind_eq; intros [].
     rewrite fold_state_ret; auto.
   Qed.
 
   Lemma fold_state_trigger_sb (e : E R) (s : S)
-    : fold_state h g (CTree.trigger e) s ~ h e s.
+    : fold_state h g (CTree.trigger e : @ctree@{_ _ _ _ d q} E C R) s ~ h e s.
   Proof.
-    unfold CTree.trigger. rewrite fold_state_vis.
+    rewrite fold_state_trigger.
     rewrite <- (bind_ret_r (h e s)) at 2.
-    cbn.
     upto_bind_eq; intros [].
-    now rewrite sb_guard, fold_state_ret.
+    now rewrite sb_guard.
   Qed.
 
+
   (** Unfolding of [interp]. *)
   Notation interp_state_ h t s :=
     (match observe t with
@@ -228,7 +240,8 @@ Section State.
 	   | BrF c k => bind (mbr (M := stateT _ _) c s) (fun xs => Guard (interp_state h (k (snd xs)) (fst xs)))
      end)%function.
 
-  Lemma unfold_interp_state `{C-<D} (t : ctree E C R) (s : S) :
+  Lemma unfold_interp_state `{C-<D}
+      (t : @ctree@{_ _ _ _ d q} E C R) (s : S) :
     interp_state h t s ≅ interp_state_ h t s.
   Proof.
     unfold interp_state, interp, MonadIter_stateT0, fold, MonadIter_ctree, Basics.iter.
@@ -254,7 +267,7 @@ Section State.
 
   Lemma equ_interp_state `{C-<D} {Q}:
     Proper (equ Q ==> eq ==> equ (eq * Q))
-           (interp_state (C := C) h (T := R)).
+           (interp_state (C := C) h (T := R) : @ctree@{_ _ _ _ d q} E C R -> _).
   Proof.
     unfold Proper, respectful.
     coinduction r IH; intros * EQ1 * <-.
@@ -272,7 +285,7 @@ Section State.
 
   #[global] Instance equ_eq_interp_state `{C-<D}:
     Proper (equ eq ==> eq ==> equ eq)
-           (interp_state (C := C) h (T := R)).
+           (interp_state (C := C) h (T := R) : @ctree@{_ _ _ _ d q} E C R -> _).
   Proof.
     cbn. intros. subst.
     eapply (equ_leq (eq * eq)%signature).
@@ -282,19 +295,21 @@ Section State.
 
   Lemma interp_state_ret `{C-<D}
         (s : S) (r : R) :
-    (interp_state (C := C) h (Ret r) s) ≅ (Ret (s, r)).
+    interp_state (C := C) h (Ret r : @ctree@{_ _ _ _ d q} E C R) s ≅
+      (Ret (s, r) : @ctree@{_ _ _ _ d' q'} F D (S * R)).
   Proof.
     rewrite ctree_eta. reflexivity.
   Qed.
 
   Lemma interp_state_stuck `{C-<D} (s : S) :
-    interp_state (C := C) (T := R) h Stuck s ≅ Stuck.
+    interp_state (C := C) h (Stuck : @ctree@{_ _ _ _ d q} E C R) s ≅
+      (Stuck : @ctree@{_ _ _ _ d' q'} F D (S * R)).
   Proof.
     now rewrite unfold_interp_state; cbn.
   Qed.
 
   Lemma interp_state_guard `{C -< D}
-    (t : ctree E C R) (s : S) :
+    (t : @ctree@{_ _ _ _ d q} E C R) (s : S) :
     interp_state h (Guard t) s ≅
     Guard (interp_state h t s).
   Proof.
@@ -302,7 +317,7 @@ Section State.
   Qed.
 
   Lemma interp_state_step `{C -< D}
-    (t : ctree E C R) (s : S) :
+    (t : @ctree@{_ _ _ _ d q} E C R) (s : S) :
     interp_state h (Step t) s ≅
     Step (Guard (interp_state h t s)).
   Proof.
@@ -310,15 +325,17 @@ Section State.
   Qed.
 
   Lemma interp_state_vis `{C-<D} {T : Type}
-    (e : E T) (k : T -> ctree E C R) (s : S) :
-    interp_state h (Vis e k) s ≅ h e s >>= fun sx => Guard (interp_state h (k (snd sx)) (fst sx)).
+    (e : E T) (k : T -> @ctree@{_ _ _ _ d q} E C R) (s : S) :
+    interp_state h (Vis e k) s ≅
+      h e s >>= fun sx => Guard (interp_state h (k (snd sx)) (fst sx)).
   Proof.
     rewrite unfold_interp_state; reflexivity.
   Qed.
 
   Lemma interp_state_br {T: Type} `{C -< D}
-    (c : C T) (k : T -> ctree E C R) (s : S) :
-    interp_state h (Br c k) s ≅ branch c >>= fun x => Guard (interp_state h (k x) s).
+    (c : C T) (k : T -> @ctree@{_ _ _ _ d q} E C R) (s : S) :
+    interp_state h (Br c k) s ≅
+      mbr c >>= fun x => Guard (interp_state h (k x) s).
   Proof.
     rewrite !unfold_interp_state; cbn.
     rewrite bind_bind.
@@ -327,10 +344,11 @@ Section State.
   Qed.
 
   Lemma interp_state_trigger `{C -< D} : forall (e : E R) st,
-  interp_state h (CTree.trigger e : ctree E C R) st ≅ x <- h e st;; Guard (Ret x).
+  interp_state h (CTree.trigger e : @ctree@{_ _ _ _ d q} E C R) st ≅
+    ((x <- h e st;; Guard (Ret x)) : @ctree@{_ _ _ _ d' q'} F D (S * R)).
   Proof.
-    intros. rewrite unfold_interp_state. cbn.
-    upto_bind. reflexivity. intros [] [] <-.
+    intros. rewrite Equ.unfold_trigger, interp_state_vis; cbn.
+    upto_bind_eq; intros [].
     now rewrite interp_state_ret.
   Qed.
 
@@ -423,7 +441,7 @@ Section State.
   Lemma refine_state_vis `{E-<F} {T : Type}
     (e : E T) (k : T -> ctree E C R) (s : S) :
     refine_state g (Vis e k) s ≅
-      trigger e >>= fun x => Guard (refine_state g (k x) s).
+      mtrigger e >>= fun x => Guard (refine_state g (k x) s).
   Proof.
     rewrite unfold_refine_state; reflexivity.
   Qed.
@@ -454,7 +472,8 @@ Qed.
 
 Section FoldBind.
   Variable (S : Type).
-  Context {E F C D : Type -> Type}.
+  Context {E : Type -> Type} {F : Type -> Type}
+          {C : Type -> Type} {D : Type -> Type}.
 
   Lemma fold_state_bind
     (h : E ~> stateT S (ctree F D))
@@ -516,7 +535,8 @@ End FoldBind.
 
 Section InterpState.
 
-Context {E F B C : Type -> Type} {X St : Type} `{HasB: B -< C}
+Context {E : Type -> Type} {F : Type -> Type}
+  {B : Type -> Type} {C : Type -> Type} {X : Type} {St : Type} `{HasB: B -< C}
   (h : E ~> stateT St (ctree F C)).
 
 Lemma epsilon_interp_state : forall (t t' : ctree E B X) s,
@@ -602,12 +622,19 @@ Proof.
     apply ssim_ret; constructor; cbn; auto.
 Qed.
 
-Definition lift_handler {E F B} (h : E ~> ctree F B) : E ~> Monads.stateT unit (ctree F B) :=
-  fun _ e s => CTree.map (fun x => (tt, x)) (h _ e).
+Section LiftHandler.
+Universes d q.
+Context {E : Type -> Type} {F : Type -> Type} {C : Type -> Type}.
+Variable h : E ~> @ctree@{_ _ _ _ d q} F C.
+
+Definition lift_handler :
+    E ~> Monads.stateT unit (@ctree@{_ _ _ _ d q} F C) :=
+  fun _ e s => CTree.map (fun x => (tt, x)) (h e).
 
-Lemma is_simple_lift_handler {E F B} (h : E ~> ctree F B) :
-  (forall Y (e : E Y), is_simple (h _ e)) ->
-  forall Y (e : E Y) st, is_simple (lift_handler h _ e st).
+
+Lemma is_simple_lift_handler :
+  (forall Y (e : E Y), is_simple (h e)) ->
+  forall Y (e : E Y) st, is_simple (lift_handler e st).
 Proof.
   intros.
   specialize (H Y e). red. destruct H; [left | right]; intros.
@@ -626,9 +653,9 @@ Qed.
 
 (* Results on interp_state can be transported to interp using interp_lift_handler. *)
 
-Lemma interp_lift_handler {E F B C X} `{HasB: B -< C}
-  (h : E ~> ctree F C) (t : ctree E B X) :
-  interp h t ≅ CTree.map (fun '(st, x) => x) (interp_state (lift_handler h) t tt).
+Lemma interp_lift_handler {B : Type -> Type} {X} `{HasB: B -< C}
+  (t : ctree E B X) :
+  interp h t ≅ CTree.map (fun '(st, x) => x) (interp_state lift_handler t tt).
 Proof.
   revert t. coinduction R CH. intros.
   pose proof @map_equ.
@@ -647,21 +674,25 @@ Proof.
     rewrite map_guard.
     constructor. apply CH.
   - rewrite interp_br, interp_state_br.
-    cbn. rewrite bind_branch, map_bind, bind_branch.
+    cbn. unfold mbr, MonadBr_ctree.
+    rewrite bind_branch, map_bind, bind_branch.
     constructor. intros.
     rewrite map_guard.
     step. constructor.
     apply CH.
 Qed.
+End LiftHandler.
+
 
 Theorem ssim_interp_h {E F1 F2 C D1 D2 X}
   `{HC1 : C -< D1} `{HC2 : C -< D2}
   (Ldest : rel (@label F1) (@label F2)) :
-  forall (h : E ~> ctree F1 D1) (h' : E ~> ctree F2 D2),
+  forall h h',
   (Ldest τ τ /\ forall (x : X), Ldest (val x) (val x)) ->
   (forall {Z} (e : E Z), h _ e (≲update_val_rel Ldest (@eq Z)) h' _ e) ->
   forall (t : ctree E C X),
-  interp h t (≲Ldest) interp h' t.
+  @interp E C (ctree F1 D1) _ _ _ _ _ _ h X t (≲Ldest)
+    @interp E C (ctree F2 D2) _ _ _ _ _ _ h' X t.
 Proof.
   intros.
   rewrite !interp_lift_handler.
@@ -882,16 +913,20 @@ Qed.
 
 (* The proof that interp preserves ssim reuses the interp_state proof. *)
 
-#[global] Instance interp_ssim_eq {E F B C X} `{HasB: B -< C} :
-  forall (h : E ~> ctree F C) (Hh : forall X e, is_simple (h X e)),
-  Proper (ssim eq ==> ssim eq) (interp (B := B) h (T := X)).
-Proof.
-  intros. cbn. intros.
-  rewrite !interp_lift_handler.
-  unfold CTree.map. apply ssim_clo_bind_eq.
-  refine (interp_state_ssim_eq _ _ _ _); auto.
-  reflexivity.
-Qed.
+#[global] Instance interp_ssim_eq@{d q d' q' +}
+  {E : Type -> Type} {F : Type -> Type} {B C : Type -> Type} {X : Type} `{HasB: B -< C}
+  (h : E ~> @ctree@{_ _ _ _ d' q'} F C)
+  (Hh : forall X (e : E X), is_simple (h _ e)) :
+  Proper (ssim eq ==> ssim eq)
+    (interp (B := B) (M := @ctree@{_ _ _ _ d' q'} F C) h (T := X) :
+      @ctree@{_ _ _ _ d q} E B X -> _).
+  Proof.
+    cbn. intros.
+    rewrite !interp_lift_handler.
+    unfold CTree.map. apply ssim_clo_bind_eq.
+    refine (interp_state_ssim_eq _ _ _ _); auto.
+    reflexivity.
+  Qed.
 
 (* Direct proof that interp_state preserves sbisim. *)
 
@@ -1026,16 +1061,20 @@ Qed.
 
 (* The proof that interp preserves sbisim reuses the interp_state proof. *)
 
-#[global] Instance interp_sbisim_eq {E F B C X} `{HasB: B -< C} :
-  forall (h : E ~> ctree F C) (Hh : forall X e, is_simple (h X e)),
-  Proper (sbisim eq ==> sbisim eq) (interp (B := B) h (T := X)).
-Proof.
-  intros. cbn. intros.
-  rewrite !interp_lift_handler.
-  unfold CTree.map. apply sbisim_clo_bind_eq.
-  refine (interp_state_sbisim_eq _ _ _ _); auto.
-  reflexivity.
-Qed.
+#[global] Instance interp_sbisim_eq@{d q d' q' +}
+  {E : Type -> Type} {F : Type -> Type} {B C : Type -> Type} {X : Type} `{HasB: B -< C}
+  (h : E ~> @ctree@{_ _ _ _ d' q'} F C)
+  (Hh : forall X (e : E X), is_simple (h _ e)) :
+  Proper (sbisim eq ==> sbisim eq)
+    (interp (B := B) (M := @ctree@{_ _ _ _ d' q'} F C) h (T := X) :
+      @ctree@{_ _ _ _ d q} E B X -> _).
+  Proof.
+    cbn. intros.
+    rewrite !interp_lift_handler.
+    unfold CTree.map. apply sbisim_clo_bind_eq.
+    refine (interp_state_sbisim_eq _ _ _ _); auto.
+    reflexivity.
+  Qed.
 
 Arguments get {S E C _}.
 Arguments put {S E C _}.
diff --git a/theories/Interp/ITree.v b/theories/Interp/ITree.v
index 985d08d..08837c8 100644
--- a/theories/Interp/ITree.v
+++ b/theories/Interp/ITree.v
@@ -1,13 +1,9 @@
-Unset Universe Checking.
 
 From Paco Require Import paco.
 
 From CTree Require Import
 	   CTree Eq Interp.Internalize Interp.FoldCTree.
 
-(* Universe issue, TO FIX *)
-Unset Universe Checking.
-Unset Auto Template Polymorphism.
 
 From ITree Require Import
 	   ITree Eq Interp InterpFacts.
@@ -18,13 +14,20 @@ Open Scope ctree.
 
 Set Implicit Arguments.
 Set Contextual Implicit.
+Set Universe Polymorphism.
 
-Definition h_embed {E C} : E ~> ctree E C :=
+Definition h_embed@{d q +} {E C} : E ~> @ctree@{_ _ _ _ d q} E C :=
   fun _ e => CTree.trigger e.
-Definition embed' {E} : itree E ~> ctree E (B01) := interp h_embed.
-Definition embed {E C} : itree (C +' E) ~> ctree E (B01 +' C) :=
+
+Definition embed'@{d q +} {E} : itree E ~> @ctree@{_ _ _ _ d q} E B01 :=
+  interp h_embed.
+
+Definition embed@{d q +} {E C} : itree (C +' E) ~> @ctree@{_ _ _ _ d q} E (B01 +' C) :=
   fun _ t => internalize (embed' t).
 
+Arguments embed' {E} [T] _.
+Arguments embed {E C} [T] _.
+
 Notation "t '-' l '→' u" := (trans l t u)
                               (at level 50, only printing,
                                 format "t  '-' l '→'  u").
@@ -45,16 +48,21 @@ Notation "t '-' l '→' u" := (transR l t u)
 #[local] Notation cVis e k  := (CTreeDefinitions.Vis e k).
 
 (** Unfolding of [interp]. *)
-Definition _interp {E F C R} (f : E ~> ctree F C) (ot : itreeF E R _)
-  : ctree F C R :=
+Section ITreeInterp.
+  Universes d q.
+Definition _interp {E F C R}
+    (f : E ~> @ctree@{_ _ _ _ d q} F C)
+    (ot : itreeF E R _) : @ctree@{_ _ _ _ d q} F C R :=
   match ot with
   | RetF r => CTreeDefinitions.Ret r
   | TauF t => cGuard (interp f t)
   | VisF e k => CTree.bind (f _ e) (fun x => cGuard (interp f (k x)))
   end.
 
-Lemma unfold_interp_ctree {E F C X} (h: E ~> ctree F C) (t : itree E X):
-  (interp h t ≅ _interp h (iobserve t))%ctree.
+Lemma unfold_interp_ctree {E F C X}
+    (f : E ~> @ctree@{_ _ _ _ d q} F C)
+    (t : itree E X) :
+  (interp f t ≅ _interp f (iobserve t))%ctree.
 Proof.
   revert t.
   coinduction R CIH.
@@ -64,8 +72,7 @@ Proof.
   destruct (iobserve t) eqn:ot; try now cbn; auto.
   match goal with
     |- equb _ _ (_cobserve ?t) (_cobserve ?u) =>
-      fold (cobserve t);
-      fold (cobserve u)
+      fold (cobserve t); fold (cobserve u)
   end.
   Transparent CTree.bind.
   cbn.
@@ -74,6 +81,7 @@ Proof.
   intros ?.
   now constructor.
 Qed.
+End ITreeInterp.
 
 #[global] Instance embed_eq {E C X}:
 	Proper (eq_itree eq ==> equ eq) (@embed E C X).
diff --git a/theories/Interp/Internalize.v b/theories/Interp/Internalize.v
index ce603ab..729c6bf 100644
--- a/theories/Interp/Internalize.v
+++ b/theories/Interp/Internalize.v
@@ -1,26 +1,29 @@
-Unset Universe Checking.
 From CTree Require Import
      CTree Eq Interp.Fold Interp.FoldCTree.
 
 Set Implicit Arguments.
 Set Contextual Implicit.
+Set Universe Polymorphism.
 
 Import CTreeNotations.
 
 Section Internalize.
-  Variable E C : Type -> Type.
+  Universes d q d' q'.
+  Variable E : Type -> Type.
+  Variable C : Type -> Type.
   Variable ExtChoice : Type -> Type.
 
-  Definition internalize_h : ExtChoice ~> ctree E (C +' ExtChoice) :=
+  Definition internalize_h : ExtChoice ~> @ctree@{_ _ _ _ d' q'} E (C +' ExtChoice) :=
     fun _ e => CTree.branchS (subevent _ e).
 
-  Definition internalize_h' : ExtChoice +' E ~> ctree E (C +' ExtChoice) :=
+  Definition internalize_h' : ExtChoice +' E ~> @ctree@{_ _ _ _ d' q'} E (C +' ExtChoice) :=
     fun _ e => match e with
             | inl1 e => internalize_h e
             | inr1 e => trigger e
             end.
 
-  Definition internalize : ctree (ExtChoice +' E) C ~> ctree E (C +' ExtChoice) :=
+  Definition internalize : @ctree@{_ _ _ _ d q} (ExtChoice +' E) C ~>
+      @ctree@{_ _ _ _ d' q'} E (C +' ExtChoice) :=
     interp internalize_h'.
 
   Lemma internalize_ret {R} (r : R) : internalize (Ret r) ≅ Ret r.
diff --git a/theories/Interp/Recursion.v b/theories/Interp/Recursion.v
index d7a1870..ca2c306 100644
--- a/theories/Interp/Recursion.v
+++ b/theories/Interp/Recursion.v
@@ -17,6 +17,8 @@ From CTree Require Import
   Misc.Pure
   Fold.
 
+Set Universe Polymorphism.
+
 Import CTreeNotations.
 Open Scope ctree_scope.
 
@@ -77,10 +79,11 @@ Open Scope ctree_scope.
 
 (** Interpret an itree in the context of a mutually recursive
     definition ([ctx]). *)
-Definition interp_mrec {D E B : Type -> Type} 
-           (ctx : D ~> ctree (D +' E) B) : ctree (D +' E) B ~> ctree E B :=
-  fun R =>
-    CTree.iter (fun t : ctree (D +' E) B R =>
+Definition interp_mrec@{d q d' q' +} {D E B}
+    (ctx : D ~> @ctree@{_ _ _ _ d q} (D +' E) B) :
+  @ctree@{_ _ _ _ d q} (D +' E) B ~> @ctree@{_ _ _ _ d' q'} E B :=
+  fun T =>
+    CTree.iter (fun t =>
       match observe t with
       | RetF r => Ret (inr r)
       | StuckF => Stuck
@@ -90,20 +93,24 @@ Definition interp_mrec {D E B : Type -> Type}
       | VisF (inr1 e) k => Vis e (fun x => Ret (inl (k x)))
       | BrF c k => Br c (fun x => Ret (inl (k x)))
       end).
-
 Arguments interp_mrec {D E B} ctx [T].
 
+
+
 (** Unfold a mutually recursive definition into separate trees,
     resolving the mutual references. *)
-Definition mrec {D E B : Type -> Type}
-           (ctx : D ~> ctree (D +' E) B) : D ~> ctree E B :=
-  fun R d => interp_mrec ctx (ctx _ d).
+
+Definition mrec@{d q d' q' +} {D E B}
+    (ctx : D ~> @ctree@{_ _ _ _ d q} (D +' E) B) :
+  D ~> @ctree@{_ _ _ _ d' q'} E B :=
+  fun T d => interp_mrec ctx (ctx T d).
 
 Arguments mrec {D E B} ctx [T].
 
 (** Make a recursive call in the handler argument of [mrec]. *)
-Definition trigger_inl1 {D E B : Type -> Type} : D ~> ctree (D +' E) B
-  := fun _ d => CTree.trigger (inl1 d).
+Definition trigger_inl1@{d q +} {D E B} :
+  D ~> @ctree@{_ _ _ _ d q} (D +' E) B :=
+  fun _ d => CTree.trigger (inl1 d).
 
 Arguments trigger_inl1 {D E B} [T].
 
@@ -125,7 +132,7 @@ Arguments trigger_inl1 {D E B} [T].
 
 (** *** Simple recursion *)
 
-Inductive callE (A B : Type) : Type -> Type :=
+Inductive callE (A : Type) (B : Type) : Type -> Type :=
 | Call : A -> callE A B B.
 
 Arguments Call {A B}.
@@ -137,35 +144,31 @@ Definition unCall {A B T} (e : callE A B T) : A :=
   end.
 
 (** Lift a function on [A] to a morphism on [callE]. *)
-Definition calling {A B} {F : Type -> Type}
-           (f : A -> F B) : callE A B ~> F :=
+Definition calling@{i +} {A B} {F : Type -> Type}
+           (f : A -> F B) : forall T : Type@{i}, callE A B T -> F T :=
   fun _ e =>
     match e with
     | Call a => f a
     end.
 
-(* TODO: This is identical to [callWith] but [rec] finds a universe
-   inconsistency with [calling], and not with [calling'].
-   The inconsistency now pops up later (currently in [Events.Env]) *)
-Definition calling' {X Y} {F B : Type -> Type}
-           (f : X -> ctree F B Y) : callE X Y ~> ctree F B :=
-  fun _ e =>
-    match e with
-    | Call a => f a
-    end.
+(** Compatibility-specialized form of [calling]. *)
+Definition calling'@{i d q +} {X Y F B}
+    (f : X -> @ctree@{_ _ _ _ d q} F B Y) :
+    forall T : Type@{i}, callE X Y T -> @ctree@{_ _ _ _ d q} F B T :=
+  calling f.
 
 (* Interpret a single recursive definition. *)
-Definition rec {E B : Type -> Type} {X Y : Type}
-           (body : X -> ctree (callE X Y +' E) B Y) :
-  X -> ctree E B Y :=
-  fun a => mrec (calling' body) (Call a).
+Definition rec@{d q +} {E B X Y}
+    (body : X -> ctree (callE X Y +' E) B Y) : X -> @ctree@{_ _ _ _ d q} E B Y :=
+  fun a => mrec (calling body) (Call a).
 
 (** An easy way to construct an event suitable for use with [rec].
     [call] is an event representing the recursive call.  Since in general, the
     function might have other events of type [E], the resulting itree has
     type [(callE A B +' E)].
 *)
-Definition call {E B X Y} (x:X) : ctree (callE X Y +' E) B Y :=
+Definition call@{d q +} {E B X Y} (x:X) :
+    @ctree@{_ _ _ _ d q} (callE X Y +' E) B Y :=
   CTree.trigger (inl1 (Call x)).
 
 (* (** Here's some syntactic sugar with a notation [mrec-fix]. *) *)
diff --git a/theories/Interp/RecursionFacts.v b/theories/Interp/RecursionFacts.v
index 203afbb..8b19d39 100644
--- a/theories/Interp/RecursionFacts.v
+++ b/theories/Interp/RecursionFacts.v
@@ -9,7 +9,6 @@ From ExtLib Require Import
      Structures.Functor
      Structures.Monad.
 
-Unset Universe Checking.
 From CTree Require Import
   CTreeDefinitions
   Eq
@@ -42,13 +41,16 @@ From ITree Require Import
 
 Import CoindNotations.
 
-Section Facts.
+Set Universe Polymorphism.
 
-Context {D E B : Type -> Type} (ctx : D ~> ctree (D +' E) B).
+Section Facts.
+Universes d q d' q' d0 q0.
+Context {D E B} (ctx : D ~> @ctree@{_ _ _ _ d q} (D +' E) B).
 
 (** Unfolding of [interp_mrec]. *)
 
-Definition _interp_mrec {R : Type} (ot : ctreeF (D +' E) B R _) : ctree E B R :=
+Definition _interp_mrec@{d' q' +} {R : Type} (ot : ctreeF (D +' E) B R _) :
+  @ctree@{_ _ _ _ d' q'} E B R :=
   match ot with
   | RetF r => Ret r
   | StuckF => Stuck
@@ -88,9 +90,11 @@ Qed.
 
 (** [mrec ctx] is equivalent to [interp (mrecursive ctx)],
     where [mrecursive] is defined as follows. *)
-Definition mrecursive (f : D ~> ctree (D +' E) B)
-  : (D +' E) ~> ctree E B :=
-  case_ (mrec f) CTree.trigger.
+Definition mrecursive@{d' q' +} (f : D ~> @ctree@{_ _ _ _ d q} (D +' E) B) :
+    (D +' E) ~> @ctree@{_ _ _ _ d' q'} E B :=
+  case_sum1 (fun _ d => mrec f d) (fun _ e => CTree.trigger e).
+Arguments mrecursive f [T] _.
+
 
 Global Instance eq_itree_mrec {R} :
   Proper (equ eq ==> equ eq) (@interp_mrec _ _ _ ctx R).
@@ -158,12 +162,12 @@ Qed.
 
 Theorem interp_mrec_trigger {U} (a : (D +' E) U) :
     interp_mrec ctx (CTree.trigger a)
-  ≲ mrecursive ctx _ a.
+  ≲ mrecursive ctx a.
 Proof.
-  rewrite unfold_interp_mrec; unfold mrecursive.
-  destruct a; cbn.
-  rewrite bind_ret_r.  apply ssim_guard_l. reflexivity.
-  unfold CTree.trigger.
+  rewrite Equ.unfold_trigger, unfold_interp_mrec; unfold mrecursive.
+  destruct a; cbn -[CTree.trigger].
+  rewrite bind_ret_r. apply ssim_guard_l. reflexivity.
+  rewrite Equ.unfold_trigger.
   apply ssim_vis_id.
   intros. split; auto.
   apply ssim_guard_l. rewrite unfold_interp_mrec. cbn.  reflexivity.
@@ -180,6 +184,7 @@ Qed.
 
 
 
+
 Theorem interp_mrec_as_interp {T} (c : ctree _ _ T) :
   interp_mrec ctx c ~ interp (mrecursive ctx) c.
 Proof.
@@ -247,7 +252,7 @@ Proof.
     apply step_sb'_guard_l'.
     intros.
     apply CIH.
-Qed.    
+Qed.
     
 
 Theorem mrec_as_interp {T} (d : D T) :
@@ -264,12 +269,11 @@ Lemma interp_trigger {E' D' F' C U} `{C -< D'} (h : E' ~> ctree F' D')  (e: E' U
   interp h (CTree.trigger e) ~ Guard (h _ e).
  *)
 
-Lemma interp_trigger {E' F' B' U} (h : E' ~> ctree F' B')  (e: E' U) :
-  interp h (@CTree.trigger _ B' _ e) ~ Guard (h _ e).
+Lemma interp_trigger {E' F' B' U}
+    (h : E' ~> @ctree@{_ _ _ _ d' q'} F' B') (e : E' U) :
+  interp h (CTree.trigger e : @ctree@{_ _ _ _ d0 q0} E' B' U) ~ Guard (h _ e).
 Proof.
-  unfold CTree.trigger.
-  rewrite interp_vis.
-  setoid_rewrite interp_ret.
+  rewrite FoldCTree.interp_trigger.
   setoid_rewrite sb_guard.
   rewrite bind_ret_r.
   reflexivity.
@@ -334,25 +338,28 @@ Local Opaque interp_mrec.
 
 (** [rec body] is equivalent to [interp (recursive body)],
     where [recursive] is defined as follows. *)
-Definition recursive {E B } {X Y} (f : X -> ctree (callE X Y +' E) B Y) : (callE X Y +' E) ~> ctree E B :=
-  case_ (calling' (rec f)) CTree.trigger.
-
-(* SAZ: TODO - update this after the change to sbisim *)
-Lemma rec_as_interp {E B} {X Y} (f : X -> ctree (callE X Y +' E) B Y) (x : X) :
-  rec f x ~ interp (recursive f) (f x).
-Proof.
-  unfold rec.
-  rewrite mrec_as_interp.
-Admitted.
-
-Lemma interp_recursive_call {E B} {X Y} (f : X -> ctree ((callE X Y) +' E) B Y) (x:X) :
-  interp (recursive f) (@call E B X Y x) ~ rec f x.
-Proof.
-  unfold recursive. unfold call.
-  rewrite interp_trigger. cbn.
-  setoid_rewrite sb_guard.
-  reflexivity.
-Qed.
+Section RecursiveFacts.
+  Context {E : Type -> Type} {B : Type -> Type} {X Y : Type}.
+  Variable f : X -> ctree (callE X Y +' E) B Y.
+
+  Definition recursive@{d q +} : (callE X Y +' E) ~> @ctree@{_ _ _ _ d q} E B :=
+    case_sum1 (calling (rec f)) (fun _ e => CTree.trigger e).
+  Arguments recursive [T] _.
+
+  (* SAZ: TODO - update this after the change to sbisim *)
+  Lemma rec_as_interp (x : X) :
+    rec f x ~ interp recursive (f x).
+  Admitted.
+
+  Lemma interp_recursive_call (x : X) :
+    interp recursive (@call E B X Y x) ~ rec f x.
+  Proof.
+    unfold recursive, call.
+    rewrite interp_trigger. cbn [case_sum1 calling].
+    setoid_rewrite sb_guard.
+    reflexivity.
+  Qed.
+End RecursiveFacts.
 
 (*
   SAZ: TODO: Not sure what the appropriate analogue of this is for ctrees
diff --git a/theories/Interp/Refine.v b/theories/Interp/Refine.v
index b497392..f82cce6 100644
--- a/theories/Interp/Refine.v
+++ b/theories/Interp/Refine.v
@@ -1,10 +1,8 @@
-Unset Universe Checking.
 
 From ExtLib Require Import
      Structures.Functor
      Structures.Monad.
 
-Unset Universe Checking.
 From CTree Require Import
      Eq
      Eq.Epsilon
@@ -13,15 +11,17 @@ From CTree Require Import
      Interp.FoldCTree
      Interp.FoldStateT
      Misc.Pure.
+Set Universe Polymorphism.
+
 
 Import ITree.Basics.Basics.Monads.
 Import MonadNotation.
 Open Scope monad_scope.
 
-Theorem ssim_pure {E F B C X} : forall (L : rel _ _) (t : ctree E B X),
+Theorem ssim_pure@{d q +} {E F B C X} : forall (L : rel _ _) (t : ctree E B X),
   pure_finite t ->
   (forall x : X, L (val x) (val tt)) ->
-  ssim L t (Ret tt : ctree F C unit).
+  ssim L t (Ret tt : @ctree@{_ _ _ _ d q} F C unit).
 Proof.
   intros. induction H; subs.
   - now apply ssim_ret.
@@ -30,7 +30,7 @@ Proof.
   - now apply ssim_guard_l.
 Qed.
 
-Unset Universe Checking.
+
 
 Theorem refine_ctree_ssim {E B B' X} :
   forall (t : ctree E B X) (h : B ~> ctree E B'),
diff --git a/theories/Misc/Head.v b/theories/Misc/Head.v
index 4af9bdd..c98d34e 100644
--- a/theories/Misc/Head.v
+++ b/theories/Misc/Head.v
@@ -23,6 +23,7 @@ Open Scope ctree_scope.
 
 Set Implicit Arguments.
 Set Contextual Implicit.
+Set Universe Polymorphism.
 
 (*|
 The [haction] computation is itself a tree. The values it computes is
@@ -32,10 +33,17 @@ The [haction] data structure captures trivially this data.
 .. coq::
 |*)
 
-Variant haction {E B X} :=
+Section haction.
+
+  Universe e.
+  Context {E : Type@{e} -> Type} {B : Type -> Type} {X : Type}.
+
+Variant haction :=
 	| ARet    (r : X)
 	| AStep   (t : ctree E B X)
-	| AVis    (Y : Type) (e : E Y) (k : Y -> ctree E B X).
+	| AVis    (Y : Type@{e}) (e : E Y) (k : Y -> ctree E B X).
+
+End haction.
 
 
 (*|
@@ -74,11 +82,11 @@ Proof.
   now step.
 Qed.
 
-Unset Universe Checking.
 
 Section trans_head.
 
-Context {E F B C : Type -> Type} {X : Type}.
+Context {E : Type -> Type} {F : Type -> Type}
+  {B : Type -> Type} {C : Type -> Type} {X : Type}.
 Context `{B -< C}.
 
 (*|
diff --git a/theories/Misc/Pure.v b/theories/Misc/Pure.v
index 8bcee8b..6bdee80 100644
--- a/theories/Misc/Pure.v
+++ b/theories/Misc/Pure.v
@@ -1,6 +1,8 @@
 From CTree Require Import
      Eq Eq.Epsilon.
 
+Set Universe Polymorphism.
+
 Variant pureb {E C X} (rec : ctree E C X -> Prop) (t : ctree E C X) : Prop :=
   | pureb_ret   (v : X) (EQ : t ≅ Ret v) : pureb rec t
   | pureb_stuck (EQ : t ≅ Stuck) : pureb rec t
@@ -15,7 +17,7 @@ Qed.
 
 Section pure.
 
-  Context {E C : Type -> Type} {X : Type}.
+  Context {E : Type -> Type} {C : Type -> Type} {X : Type}.
 
   Class pure (t : ctree E C X) := pure_ : gfp (@fpure E C X) t.
 
@@ -144,7 +146,7 @@ Qed.
 
 Section pure_finite.
 
-  Context {E C : Type -> Type} {X : Type}.
+  Context {E : Type -> Type} {C : Type -> Type} {X : Type}.
 
   Inductive pure_finite_ : ctree E C X -> Prop :=
   | puref_ret (v : X) t (EQ: t ≅ Ret v) : pure_finite_ t
@@ -249,7 +251,7 @@ Class is_simple {E C X} (t : ctree E C X) :=
 
 Section is_simple_theory.
 
-  Context {E C : Type -> Type} {X : Type}.
+  Context {E : Type -> Type} {C : Type -> Type} {X : Type}.
 
   #[global] Instance is_simple_equ :
     Proper (equ eq ==> iff) (@is_simple E C X).
diff --git a/theories/dune b/theories/dune
index 8165e1a..586867f 100644
--- a/theories/dune
+++ b/theories/dune
@@ -1,5 +1,6 @@
 (include_subdirs qualified)
 
-(coq.theory
+(rocq.theory
  (name CTree)
- (package rocq-ctree))
+ (package rocq-ctree)
+ (theories Stdlib ExtLib Paco ITree Coinduction RelationAlgebra))