diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index 4705a8c..b5719af 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -19,6 +19,8 @@ jobs:
     strategy:
       matrix:
         image:
+          - 'mathcomp/mathcomp:2.2.0-coq-8.19'
+          - 'mathcomp/mathcomp:2.2.0-coq-8.18'
           - 'mathcomp/mathcomp:2.2.0-coq-8.17'
           - 'mathcomp/mathcomp:2.2.0-coq-8.16'
           - 'mathcomp/mathcomp:2.1.0-coq-8.17'
diff --git a/README.md b/README.md
index a5e8964..7080808 100644
--- a/README.md
+++ b/README.md
@@ -52,7 +52,7 @@ of said algorithm.
 - Coq-community maintainer(s):
   - Christian Doczkal ([**@chdoc**](https://github.com/chdoc))
 - License: [CeCILL-B](LICENSE)
-- Compatible Coq versions: 8.16 and 8.17
+- Compatible Coq versions: 8.16 to 8.20
 - Additional dependencies:
   - [MathComp](https://math-comp.github.io) 2.0 or later (`ssreflect` suffices)
   - [Hierarchy Builder](https://github.com/math-comp/hierarchy-builder) 1.6.0 or later
diff --git a/_CoqProject b/_CoqProject
index 8f8da5e..4c6d636 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -3,7 +3,6 @@
 -arg -w -arg -notation-overridden
 -arg -w -arg -redundant-canonical-projection
 -arg -w -arg -notation-incompatible-format
--arg -w -arg -deprecated-instance-without-locality
 
 -Q theories CompDecModal
 
diff --git a/coq-comp-dec-modal.opam b/coq-comp-dec-modal.opam
index 2a0b8d9..e3439be 100644
--- a/coq-comp-dec-modal.opam
+++ b/coq-comp-dec-modal.opam
@@ -32,7 +32,7 @@ of said algorithm.
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {>= "8.16" & < "8.18"}
+  "coq" {>= "8.16" & < "8.21"}
   "coq-mathcomp-ssreflect" {>= "2.0"}
   "coq-hierarchy-builder" {>= "1.6.0"}
 ]
diff --git a/meta.yml b/meta.yml
index 07ed94b..60734ef 100644
--- a/meta.yml
+++ b/meta.yml
@@ -52,10 +52,14 @@ license:
   identifier: CECILL-B
 
 supported_coq_versions:
-  text: 8.16 and 8.17
-  opam: '{>= "8.16" & < "8.18"}'
+  text: 8.16 to 8.20
+  opam: '{>= "8.16" & < "8.21"}'
 
 tested_coq_opam_versions:
+- version: '2.2.0-coq-8.19'
+  repo: 'mathcomp/mathcomp'
+- version: '2.2.0-coq-8.18'
+  repo: 'mathcomp/mathcomp'
 - version: '2.2.0-coq-8.17'
   repo: 'mathcomp/mathcomp'
 - version: '2.2.0-coq-8.16'
diff --git a/theories/CPDL/PDL_def.v b/theories/CPDL/PDL_def.v
index af7a723..7837d0b 100644
--- a/theories/CPDL/PDL_def.v
+++ b/theories/CPDL/PDL_def.v
@@ -4,7 +4,7 @@ From HB Require Import structures.
 Require Import Relations Lia Setoid Morphisms.
 From mathcomp Require Import all_ssreflect.
 From CompDecModal.libs 
- Require Import edone bcase fset base modular_hilbert sltype rewrite_inequality fset_tac.
+ Require Import edone bcase fset base induced_sym modular_hilbert sltype rewrite_inequality fset_tac.
 
 Set Default Proof Using "Type".
 
@@ -323,7 +323,7 @@ End Hilbert.
   Lemma rNorm p s t : prv (s ---> t) -> prv ([p]s ---> [p]t).
   Proof. move => H. rule axN. exact: rNec. Qed.
 
-  Instance AX_mor (p : prog) : Proper (@mImpPrv prv_mSystem ==> @mImpPrv prv_mSystem) (fAX p).
+  #[export] Instance AX_mor (p : prog) : Proper (@mImpPrv prv_mSystem ==> @mImpPrv prv_mSystem) (fAX p).
   Proof. exact: rNorm. Qed.
 
   Lemma rStar_ind p u s : prv (u ---> [p]u) -> prv (u ---> s) -> prv (u ---> [p^*]s).
@@ -344,7 +344,7 @@ End Hilbert.
   Lemma rEXn p s t : prv (s ---> t) -> prv (EX p s ---> EX p t).
   Proof. move => H. rule ax_contraNN. apply: rNorm. by rule ax_contraNN. Qed.
 
-  Instance EX_mor (p : prog) : Proper (@mImpPrv prv_mSystem ==> @mImpPrv prv_mSystem) (EX p).
+  #[export] Instance EX_mor (p : prog) : Proper (@mImpPrv prv_mSystem ==> @mImpPrv prv_mSystem) (EX p).
   Proof. exact: rEXn. Qed.
 
   Lemma axDBD p s t : prv (EX p s ---> [p]t ---> EX p (s :/\: t)).
diff --git a/theories/CPDL/hilbert_ref.v b/theories/CPDL/hilbert_ref.v
index fedee99..d23d065 100644
--- a/theories/CPDL/hilbert_ref.v
+++ b/theories/CPDL/hilbert_ref.v
@@ -3,7 +3,7 @@
 Require Import Relations.
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp Require Import all_ssreflect.
-From CompDecModal.libs Require Import edone bcase fset base modular_hilbert.
+From CompDecModal.libs Require Import edone bcase fset base induced_sym modular_hilbert.
 From CompDecModal.CPDL Require Import PDL_def demo.
 
 Set Default Proof Using "Type".
diff --git a/theories/CTL/gen_hsound.v b/theories/CTL/gen_hsound.v
index 5197bd2..0afddcc 100644
--- a/theories/CTL/gen_hsound.v
+++ b/theories/CTL/gen_hsound.v
@@ -3,7 +3,7 @@
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp Require Import all_ssreflect.
 From CompDecModal.libs
- Require Import edone bcase fset base modular_hilbert sltype.
+ Require Import edone bcase fset base induced_sym modular_hilbert sltype.
 From CompDecModal.CTL
  Require Import CTL_def gen_def hilbert hilbert_hist.
 Import IC.
diff --git a/theories/CTL/hilbert_Eme90.v b/theories/CTL/hilbert_Eme90.v
index e78e42a..f2952fb 100644
--- a/theories/CTL/hilbert_Eme90.v
+++ b/theories/CTL/hilbert_Eme90.v
@@ -3,7 +3,7 @@
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp Require Import all_ssreflect.
 From CompDecModal.libs
- Require Import edone bcase fset base modular_hilbert.
+ Require Import edone bcase fset base induced_sym modular_hilbert.
 From CompDecModal.CTL
  Require Import CTL_def hilbert.
 
diff --git a/theories/CTL/hilbert_LS.v b/theories/CTL/hilbert_LS.v
index 0ba9bfb..e99a612 100644
--- a/theories/CTL/hilbert_LS.v
+++ b/theories/CTL/hilbert_LS.v
@@ -3,7 +3,7 @@
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp Require Import all_ssreflect.
 From CompDecModal.libs
- Require Import edone bcase fset base modular_hilbert.
+ Require Import edone bcase fset base induced_sym modular_hilbert.
 From CompDecModal.CTL
  Require Import CTL_def hilbert hilbert_hist.
 
@@ -202,4 +202,4 @@ Proof.
 Qed.       
 
 Lemma LS_sound s : LS.prv s -> prv s.
-Proof. elim => {s} *; eauto using prv,ERel,ARel,axARf,axERf,axAUcmp,axSer. Qed.
\ No newline at end of file
+Proof. elim => {s} *; eauto using prv,ERel,ARel,axARf,axERf,axAUcmp,axSer. Qed.
diff --git a/theories/CTL/hilbert_hist.v b/theories/CTL/hilbert_hist.v
index 1ca3449..02878d2 100644
--- a/theories/CTL/hilbert_hist.v
+++ b/theories/CTL/hilbert_hist.v
@@ -3,7 +3,7 @@
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp Require Import all_ssreflect.
 From CompDecModal.libs
- Require Import edone bcase fset base modular_hilbert sltype.
+ Require Import edone bcase fset base induced_sym modular_hilbert sltype.
 From CompDecModal.CTL
  Require Import CTL_def hilbert.
 Import IC.
diff --git a/theories/CTL/hilbert_ref.v b/theories/CTL/hilbert_ref.v
index 8db4cbb..2d00bd2 100644
--- a/theories/CTL/hilbert_ref.v
+++ b/theories/CTL/hilbert_ref.v
@@ -4,7 +4,7 @@ Require Import Lia.
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp Require Import all_ssreflect.
 From CompDecModal.libs
- Require Import edone bcase fset base modular_hilbert sltype.
+ Require Import edone bcase fset base induced_sym modular_hilbert sltype.
 From CompDecModal.CTL
  Require Import CTL_def dags demo hilbert relaxed_pruning.
 Import IC.
diff --git a/theories/K/gentzen.v b/theories/K/gentzen.v
index b910927..565685d 100644
--- a/theories/K/gentzen.v
+++ b/theories/K/gentzen.v
@@ -4,7 +4,7 @@ Require Import Lia.
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp Require Import all_ssreflect.
 From CompDecModal.libs
- Require Import edone bcase fset base modular_hilbert sltype.
+ Require Import edone bcase fset base induced_sym modular_hilbert sltype.
 From CompDecModal.K
  Require Import K_def demo.
 
diff --git a/theories/K/hilbert_ref.v b/theories/K/hilbert_ref.v
index c96f018..11fdd62 100644
--- a/theories/K/hilbert_ref.v
+++ b/theories/K/hilbert_ref.v
@@ -4,7 +4,7 @@ Require Import Lia.
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp Require Import all_ssreflect.
 From CompDecModal.libs
- Require Import edone bcase fset base modular_hilbert sltype.
+ Require Import edone bcase fset base induced_sym modular_hilbert sltype.
 From CompDecModal.K
  Require Import K_def demo.
 
diff --git a/theories/Kstar/hilbert_ref.v b/theories/Kstar/hilbert_ref.v
index feec0b7..264bdb0 100644
--- a/theories/Kstar/hilbert_ref.v
+++ b/theories/Kstar/hilbert_ref.v
@@ -4,7 +4,7 @@ Require Import Relations Lia.
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp Require Import all_ssreflect.
 From CompDecModal.libs
- Require Import edone bcase fset base modular_hilbert sltype.
+ Require Import edone bcase fset base induced_sym modular_hilbert sltype.
 From CompDecModal.Kstar
  Require Import Kstar_def demo.
 
diff --git a/theories/PDL/PDL_def.v b/theories/PDL/PDL_def.v
index 02f05fa..8607bb6 100644
--- a/theories/PDL/PDL_def.v
+++ b/theories/PDL/PDL_def.v
@@ -4,7 +4,7 @@ From HB Require Import structures.
 Require Import Relations Lia Setoid Morphisms.
 From mathcomp Require Import all_ssreflect.
 From CompDecModal.libs 
- Require Import edone bcase fset base modular_hilbert sltype rewrite_inequality fset_tac.
+ Require Import edone bcase fset base induced_sym modular_hilbert sltype rewrite_inequality fset_tac.
 
 Set Default Proof Using "Type".
 
@@ -310,7 +310,7 @@ End Hilbert.
   Lemma rNorm p s t : prv (s ---> t) -> prv ([p]s ---> [p]t).
   Proof. move => H. rule axN. exact: rNec. Qed.
 
-  Instance AX_mor (p : prog) : Proper (@mImpPrv prv_mSystem ==> @mImpPrv prv_mSystem) (fAX p).
+  #[export] Instance AX_mor (p : prog) : Proper (@mImpPrv prv_mSystem ==> @mImpPrv prv_mSystem) (fAX p).
   Proof. exact: rNorm. Qed.
 
   Lemma rStar_ind p u s : prv (u ---> [p]u) -> prv (u ---> s) -> prv (u ---> [p^*]s).
diff --git a/theories/PDL/hilbert_ref.v b/theories/PDL/hilbert_ref.v
index dff8aea..f96ca28 100644
--- a/theories/PDL/hilbert_ref.v
+++ b/theories/PDL/hilbert_ref.v
@@ -3,7 +3,7 @@
 Require Import Relations.
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp Require Import all_ssreflect.
-From CompDecModal.libs Require Import edone bcase fset base modular_hilbert.
+From CompDecModal.libs Require Import edone bcase fset base induced_sym modular_hilbert.
 From CompDecModal.PDL Require Import PDL_def demo.
 
 Set Default Proof Using "Type".
diff --git a/theories/libs/edone.v b/theories/libs/edone.v
index d121c42..9e096d1 100644
--- a/theories/libs/edone.v
+++ b/theories/libs/edone.v
@@ -21,7 +21,6 @@ Ltac done := trivial; hnf in |- *; intros;
       | split
       | rewrite ?andbT ?andbF ?orbT ?orbF ]
     )
-    | case not_locked_false_eq_true; assumption
     | match goal with
         | H:~ _ |- _ => solve [ case H; trivial ]
       end
diff --git a/theories/libs/induced_sym.v b/theories/libs/induced_sym.v
index f10a91b..66f5632 100644
--- a/theories/libs/induced_sym.v
+++ b/theories/libs/induced_sym.v
@@ -12,7 +12,7 @@ Require Import Setoid Morphisms Basics.
 Class InducedSym {T : Type} (P R : relation T) :=
   induced_iff : forall x y, R x y <-> P x y /\ P y x.
 
-Instance induced_sub {T : Type} (P R : relation T) :
+#[export] Instance induced_sub {T : Type} (P R : relation T) :
   InducedSym P R -> subrelation R P.
 Proof. firstorder. Qed.
 
@@ -45,22 +45,22 @@ Proof.
   firstorder.
 Qed.
 
-Instance induced_mor_p {T : Type} (P R : relation T) m :
+#[export] Instance induced_mor_p {T : Type} (P R : relation T) m :
   InducedSym P R -> Proper (P ==> P) m -> Proper (R ==> R) m.
 Proof. intros ind prop x y Rxy; induced_tac R. Qed.
 
-Instance induced_mor_n {T : Type} (P R : relation T) m :
+#[export] Instance induced_mor_n {T : Type} (P R : relation T) m :
   InducedSym P R -> Proper (P --> P) m -> Proper (R ==> R) m.
 Proof. intros ind prop x y Rxy; induced_tac R. Qed.
 
-Instance induced_mor_pp {T : Type} (P R : relation T) m :
+#[export] Instance induced_mor_pp {T : Type} (P R : relation T) m :
   InducedSym P R -> Proper (P ==> P ==> P) m -> Proper (R ==> R ==> R) m.
 Proof. intros ind prop x y Rxy x' y' Rxy'; induced_tac R. Qed.
 
-Instance induced_mor_pn {T : Type} (P R : relation T) m :
+#[export] Instance induced_mor_pn {T : Type} (P R : relation T) m :
   InducedSym P R -> Proper (P ==> P --> P) m -> Proper (R ==> R ==> R) m.
 Proof. intros ind prop x y Rxy x' y' Rxy'; induced_tac R. Qed.
 
-Instance induced_mor_np {T : Type} (P R : relation T) m :
+#[export] Instance induced_mor_np {T : Type} (P R : relation T) m :
   InducedSym P R -> Proper (P --> P ==> P) m -> Proper (R ==> R ==> R) m.
 Proof. intros ind prop x y Rxy x' y' Rxy'; induced_tac R. Qed.
diff --git a/theories/libs/modular_hilbert.v b/theories/libs/modular_hilbert.v
index 5790308..1019164 100644
--- a/theories/libs/modular_hilbert.v
+++ b/theories/libs/modular_hilbert.v
@@ -102,14 +102,14 @@ Ltac Suff u := apply (mp2 (axS u _ _)).
 
 (** Enable Setoid rewriting for with provable implications *)
 
-Instance mImpPrv_rel (mS : mSystem) : PreOrder (@mImpPrv mS).
+#[export] Instance mImpPrv_rel (mS : mSystem) : PreOrder (@mImpPrv mS).
 Proof. split. exact: axI. exact: mImpPrv_trans. Qed.
 
-Instance mprv_mor (mS : mSystem) :
+#[export] Instance mprv_mor (mS : mSystem) :
   Proper ((@mImpPrv mS) ++> Basics.impl) (@mprv mS).
 Proof. move => x y H H'. mp; eassumption. Qed.
 
-Instance Imp_mor (mS : mSystem) :
+#[export] Instance Imp_mor (mS : mSystem) :
   Proper ((@mImpPrv mS) --> (@mImpPrv mS) ++> (@mImpPrv mS)) (@Imp mS).
 Proof.
   move => x' x X y y' Y. rewrite /mImpPrv in X Y *.
@@ -208,15 +208,15 @@ End PTheoryBase.
 
 (** Morphisms for defined locial operators *)
 
-Instance Neg_mor (pS : pSystem) :
+#[export] Instance Neg_mor (pS : pSystem) :
   Proper ((@mImpPrv pS) --> (@mImpPrv pS))(@Neg pS).
 Proof. rewrite /Neg; solve_proper. Qed.
 
-Instance And_mor (pS : pSystem) :
+#[export] Instance And_mor (pS : pSystem) :
   Proper ((@mImpPrv pS) ==> (@mImpPrv pS) ==> (@mImpPrv pS)) (@And pS).
 Proof. by rewrite /And; solve_proper. Qed.
 
-Instance Or_mor (pS : pSystem) :
+#[export] Instance Or_mor (pS : pSystem) :
   Proper ((@mImpPrv pS) ==> (@mImpPrv pS) ==> (@mImpPrv pS)) (@Or pS).
 Proof. by rewrite /Or; solve_proper. Qed.
 
@@ -243,35 +243,35 @@ Section EqiTheoryBase.
   Proof. exact: axAI. Qed.
 End EqiTheoryBase.
 
-Instance eqi_induced_symmety (pS : pSystem) : InducedSym (@mImpPrv pS) (@EqiPrv pS).
+#[export] Instance eqi_induced_symmety (pS : pSystem) : InducedSym (@mImpPrv pS) (@EqiPrv pS).
 Proof.
   move => s t. split => [H | [H1 H2]].
   split. by rule axEEl. by rule axEEr. by rule axEI.
 Qed.
 
-Instance induced_eqi (pS : pSystem) : Equivalence (@EqiPrv pS).
+#[export] Instance induced_eqi (pS : pSystem) : Equivalence (@EqiPrv pS).
 Proof. apply: induced_eqi. Qed.
 
 (** Short cut morphisms for faster equivalence rewrites *)
-Instance mprv_eqi_mor (pS : pSystem) :
+#[export] Instance mprv_eqi_mor (pS : pSystem) :
   Proper (@EqiPrv pS ==> iff) (@mprv pS).
 Proof. move => s t H. split. by rewrite -> H. by rewrite <- H. Qed.
 
-Instance Neg_Eqi_mor (pS : pSystem) :
+#[export] Instance Neg_Eqi_mor (pS : pSystem) :
   Proper ((@EqiPrv pS) ==> (@EqiPrv pS))(@Neg pS).
 Proof. rewrite /Neg; solve_proper. Qed.
 
-Instance And_Eqi_mor (pS : pSystem) :
+#[export] Instance And_Eqi_mor (pS : pSystem) :
   Proper ((@EqiPrv pS) ==> (@EqiPrv pS) ==> (@EqiPrv pS)) (@And pS).
 Proof. by rewrite /And; solve_proper. Qed.
 
-Instance Or_Eqi_mor (pS : pSystem) :
+#[export] Instance Or_Eqi_mor (pS : pSystem) :
   Proper ((@EqiPrv pS) ==> (@EqiPrv pS) ==> (@EqiPrv pS)) (@Or pS).
 Proof. by rewrite /Or; solve_proper. Qed.
 
 (** Rewriting below Equivalences *)
 
-Instance Eqi_mor (pS : pSystem) :
+#[export] Instance Eqi_mor (pS : pSystem) :
   Proper ((@EqiPrv pS) ==> (@EqiPrv pS) ==> (@EqiPrv pS)) (@Eqi pS).
 Proof. rewrite /Eqi. solve_proper. Qed.
 
@@ -518,20 +518,20 @@ Record kSystem := KSystem { psort   :> pSystem;
 Lemma rNorm (kS : kSystem) (s t : kS) : mprv (s ---> t) -> mprv (AX s ---> AX t).
 Proof. move => H. rule axN. exact: rNec. Qed.
 
-Instance AX_mor (kS : kSystem) : Proper ((@mImpPrv kS) ==> (@mImpPrv kS)) (@AX kS).
+#[export] Instance AX_mor (kS : kSystem) : Proper ((@mImpPrv kS) ==> (@mImpPrv kS)) (@AX kS).
 Proof. exact: rNorm. Qed.
 
 Definition EX (kS : kSystem) (s : kS) := ~~: AX (~~: s).
 
-Instance EX_mor (kS : kSystem) : Proper ((@mImpPrv kS) ==> (@mImpPrv kS)) (@EX kS).
+#[export] Instance EX_mor (kS : kSystem) : Proper ((@mImpPrv kS) ==> (@mImpPrv kS)) (@EX kS).
 Proof. move => x y H. rewrite /EX /mImpPrv. by rewrite -> H. Qed.
 
 (** Redundant Morphisms for Equivalence *)
 
-Instance AX_Eqi_mor (kS : kSystem) : Proper ((@EqiPrv kS) ==> (@EqiPrv kS)) (@AX kS).
+#[export] Instance AX_Eqi_mor (kS : kSystem) : Proper ((@EqiPrv kS) ==> (@EqiPrv kS)) (@AX kS).
 Proof. move => s t H. rewrite -> H. reflexivity. Qed.
 
-Instance EX_Eqi_mor (kS : kSystem) : Proper ((@EqiPrv kS) ==> (@EqiPrv kS)) (@EX kS).
+#[export] Instance EX_Eqi_mor (kS : kSystem) : Proper ((@EqiPrv kS) ==> (@EqiPrv kS)) (@EX kS).
 Proof. move => s t H. rewrite -> H. reflexivity. Qed.
 
 Section KTheory.
@@ -609,7 +609,7 @@ Section KStarTheory.
   Lemma rNormS s t : mprv (s ---> t) -> mprv (AG s ---> AG t).
   Proof. move/rNecS. apply: rMP. exact: axAGN. Qed.
 
-  Instance AG_mor : Proper ((@mImpPrv ksS) ==> (@mImpPrv ksS)) (@AG ksS).
+  #[export] Instance AG_mor : Proper ((@mImpPrv ksS) ==> (@mImpPrv ksS)) (@AG ksS).
   Proof. exact: rNormS. Qed.
 
   Lemma axAGEn s : mprv (~~: AG s ---> ~~: s :\/: ~~: AX (AG s)).
@@ -649,25 +649,25 @@ Definition ER {cS : ctlSystem} (s t : cS) := ~~: AU (~~: s) (~~: t).
 Definition EU {cS : ctlSystem} (s t : cS) := ~~: AR (~~: s) (~~: t).
 Notation "'EG' s" := (ER Bot s) (at level 8).
 
-Instance AU_mor (cS : ctlSystem) :
+#[export] Instance AU_mor (cS : ctlSystem) :
   Proper ((@mImpPrv cS) ==> (@mImpPrv cS) ==> (@mImpPrv cS))(@AU cS).
 Proof.
   move => x x' X y y' Y. rewrite /mImpPrv in X Y *.
   apply: rAU_ind. rewrite -> Y. exact: axAUI. rewrite -> X. exact: axAUf.
 Qed.
 
-Instance ER_mor (cS : ctlSystem) :
+#[export] Instance ER_mor (cS : ctlSystem) :
   Proper ((@mImpPrv cS) ==> (@mImpPrv cS) ==> (@mImpPrv cS))(@ER cS).
 Proof. rewrite /ER. solve_proper. Qed.
 
-Instance AR_mor (cS : ctlSystem) :
+#[export] Instance AR_mor (cS : ctlSystem) :
   Proper ((@mImpPrv cS) ==> (@mImpPrv cS) ==> (@mImpPrv cS))(@AR cS).
 Proof.
   move => x x' X y y' Y. rewrite /mImpPrv in X Y *.
   apply: rAR_ind. rewrite <- Y. exact: axARE. rewrite <- X. exact: axARu.
 Qed.
 
-Instance EU_mor (cS : ctlSystem) :
+#[export] Instance EU_mor (cS : ctlSystem) :
   Proper ((@mImpPrv cS) ==> (@mImpPrv cS) ==> (@mImpPrv cS))(@EU cS).
 Proof. rewrite /EU. solve_proper. Qed.
 
diff --git a/theories/libs/rewrite_inequality.v b/theories/libs/rewrite_inequality.v
index 087f336..6bfa55c 100644
--- a/theories/libs/rewrite_inequality.v
+++ b/theories/libs/rewrite_inequality.v
@@ -17,30 +17,30 @@ Inductive leb a b := Leb of (a ==> b).
 Lemma leb_eq a b : leb a b <-> (a -> b). 
 Proof. move: a b => [|] [|]; firstorder. Qed.
 
-Instance: PreOrder leb.
+#[export] Instance: PreOrder leb.
 Proof. split => [[|]|[|][|][|][?][?]]; try exact: Leb. Qed.
 
-Instance: Proper (leb ==> leb ==> leb) andb.
+#[export] Instance: Proper (leb ==> leb ==> leb) andb.
 Proof. move => [|] [|] [A] c d [B]; exact: Leb. Qed.
 
-Instance: Proper (leb ==> leb ==> leb) orb.
+#[export] Instance: Proper (leb ==> leb ==> leb) orb.
 Proof. move => [|] [|] [A] [|] d [B]; exact: Leb. Qed.
 
-Instance: Proper (leb ==> impl) is_true.
+#[export] Instance: Proper (leb ==> impl) is_true.
 Proof. move => a b []. exact: implyP. Qed.
 
 (** Instances for le  *)
 
-Instance: Proper (le --> le ++> leb) leq. 
+#[export] Instance: Proper (le --> le ++> leb) leq. 
 Proof. move => n m /leP ? n' m' /leP ?. apply/leb_eq => ?. eauto using leq_trans. Qed.
 
-Instance: Proper (le ==> le ==> le) addn. 
+#[export] Instance: Proper (le ==> le ==> le) addn. 
 Proof. move => n m /leP ? n' m' /leP ?. apply/leP. exact: leq_add. Qed.
 
-Instance: Proper (le ++> le --> le) subn.
+#[export] Instance: Proper (le ++> le --> le) subn.
 Proof. move => n m /leP ? n' m' /leP ?. apply/leP. exact: leq_sub. Qed.
 
-Instance: RewriteRelation le. Qed.
+#[export] Instance: RewriteRelation le. Qed.
 
 (** Wrapper Lemma to trigger setoid rewrite *)
 Definition leqRW m n  : m <= n -> le m n := leP.
diff --git a/theories/libs/sltype.v b/theories/libs/sltype.v
index c2f2086..8a8fd2f 100644
--- a/theories/libs/sltype.v
+++ b/theories/libs/sltype.v
@@ -1,7 +1,7 @@
 (* (c) Copyright Christian Doczkal, Saarland University                   *)
 (* Distributed under the terms of the CeCILL-B license                    *)
 From mathcomp Require Import all_ssreflect.
-From CompDecModal.libs Require Import edone bcase fset base modular_hilbert.
+From CompDecModal.libs Require Import edone bcase fset base induced_sym modular_hilbert.
 
 Set Default Proof Using "Type".