diff --git a/_CoqProject b/_CoqProject
index e85977336776f44a7d0c30417fbe2bbf937151b5..15c320d40b62c44460de97b2402ee17b9132c631 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,10 +1,11 @@
 -Q theories osiris
 -arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
-theories/typing/side.v
-theories/typing/stype.v
+theories/base_logic/auth_excl.v
+theories/encodings/involutive.v
+theories/encodings/side.v
+theories/encodings/stype_def.v
 theories/encodings/encodable.v
 theories/encodings/list.v
-theories/encodings/auth_excl.v
 theories/encodings/channel.v
 theories/encodings/stype.v
 theories/encodings/stype_enc.v
diff --git a/theories/encodings/auth_excl.v b/theories/base_logic/auth_excl.v
similarity index 100%
rename from theories/encodings/auth_excl.v
rename to theories/base_logic/auth_excl.v
diff --git a/theories/encodings/channel.v b/theories/encodings/channel.v
index fa0ed8a70d9937e4154f3fe73410bfd9c489ace7..c9feffb00e066a8127a073bf1dbe2919f5e64665 100644
--- a/theories/encodings/channel.v
+++ b/theories/encodings/channel.v
@@ -5,8 +5,9 @@ From iris.heap_lang Require Import proofmode notation.
 From iris.algebra Require Import excl auth list.
 From iris.base_logic.lib Require Import auth.
 From iris.heap_lang.lib Require Import spin_lock.
-From osiris.typing Require Export side.
-From osiris.encodings Require Import list auth_excl.
+From osiris.base_logic Require Import auth_excl.
+From osiris.encodings Require Export side.
+From osiris.encodings Require Import list.
 Set Default Proof Using "Type".
 Import uPred.
 
diff --git a/theories/typing/side.v b/theories/encodings/side.v
similarity index 86%
rename from theories/typing/side.v
rename to theories/encodings/side.v
index 1c418d8e7e474e88e0d3019704fbc8637fb15422..f58a57b7dc7de2062f07ac76cf66e06a01344b2a 100644
--- a/theories/typing/side.v
+++ b/theories/encodings/side.v
@@ -1,5 +1,5 @@
 From iris.heap_lang Require Import proofmode notation.
-From osiris.typing Require Export involutive.
+From osiris.encodings Require Export involutive.
 
 Inductive side := Left | Right.
 Instance side_inhabited : Inhabited side := populate Left.
diff --git a/theories/encodings/stype.v b/theories/encodings/stype.v
index dc38fddd33cb1c60a277e2091c9d06ddbaa0c4ba..6cdfac0a34fc71302fbc0f2158c1130df2af3ad7 100644
--- a/theories/encodings/stype.v
+++ b/theories/encodings/stype.v
@@ -5,8 +5,8 @@ From iris.heap_lang Require Import proofmode notation.
 From iris.heap_lang.lib Require Import spin_lock.
 From iris.algebra Require Import list auth excl.
 From iris.base_logic Require Import invariants.
-From osiris.typing Require Export stype.
-From osiris.encodings Require Import auth_excl.
+From osiris.base_logic Require Import auth_excl.
+From osiris.encodings Require Export stype_def.
 From osiris.encodings Require Export channel.
 
 Class logrelG A Σ := {
diff --git a/theories/typing/stype.v b/theories/encodings/stype_def.v
similarity index 99%
rename from theories/typing/stype.v
rename to theories/encodings/stype_def.v
index da45f6417ddbe19eb015ab9fd5774f4c3d34978b..3a82661db9160c780acbcb853ab5259316b770d8 100644
--- a/theories/typing/stype.v
+++ b/theories/encodings/stype_def.v
@@ -4,11 +4,9 @@ From stdpp Require Export list.
 From iris.base_logic Require Import base_logic.
 From iris.algebra Require Import updates local_updates.
 From iris.heap_lang Require Import proofmode notation.
+From osiris.encodings Require Import involutive.
 Set Default Proof Using "Type".
 
-Class Involutive {A} (R : relation A) (f : A → A) :=
-  involutive x : R (f (f x)) x.
-
 Inductive action := Send | Receive.
 Instance action_inhabited : Inhabited action := populate Send.
 Definition dual_action (a : action) : action :=
diff --git a/theories/examples/branching_examples.v b/theories/examples/branching_examples.v
index bd75583c951a3c6362853ab6f216bb0e47b59c7b..8b7431303224733e3acad7b901bff3fd9c9e64f3 100644
--- a/theories/examples/branching_examples.v
+++ b/theories/examples/branching_examples.v
@@ -1,7 +1,6 @@
 From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Import proofmode notation.
-From osiris.typing Require Import side stype.
 From osiris.encodings Require Import channel branching.
 From iris.base_logic Require Import invariants.
 
diff --git a/theories/examples/branching_proofs.v b/theories/examples/branching_proofs.v
index a7cadc1c51158bbf47b14be8857790f404a87128..5226ad6dba555dd93b1aad0038c151b6517e65a2 100644
--- a/theories/examples/branching_proofs.v
+++ b/theories/examples/branching_proofs.v
@@ -2,7 +2,6 @@ From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Import proofmode notation.
 From iris.base_logic Require Import invariants.
-From osiris.typing Require Import side stype.
 From osiris.encodings Require Import branching.
 From osiris.examples Require Import branching_examples.
 
diff --git a/theories/examples/examples.v b/theories/examples/examples.v
index f5db63f211838b64214438b67c174c7e9ae99b51..b40881be53765f31be873e98871b00936b0e8af3 100644
--- a/theories/examples/examples.v
+++ b/theories/examples/examples.v
@@ -1,8 +1,7 @@
 From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Import proofmode notation.
-From osiris.typing Require Import side stype.
-From osiris.encodings Require Import channel stype.
+From osiris.encodings Require Import stype.
 From iris.base_logic Require Import invariants.
 
 Section Examples.
diff --git a/theories/examples/list_sort.v b/theories/examples/list_sort.v
index 9d2c7643e01a6cac0a7cbebf5273efb58d2ead80..c235b9ab036806ccd6b68a39f7c30e7a85828e6f 100644
--- a/theories/examples/list_sort.v
+++ b/theories/examples/list_sort.v
@@ -1,7 +1,6 @@
 From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Import proofmode notation.
-From osiris.typing Require Import side stype.
 From osiris.encodings Require Import list channel stype_enc.
 From iris.base_logic Require Import invariants.
 From stdpp Require Import sorting.
diff --git a/theories/examples/proofs.v b/theories/examples/proofs.v
index 262c6756a2ca95df9ae596bc3d84546cf481082e..8254e5384473b0ebc8ac06f992e287ef5b70417d 100644
--- a/theories/examples/proofs.v
+++ b/theories/examples/proofs.v
@@ -2,7 +2,6 @@ From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Import proofmode notation.
 From iris.base_logic Require Import invariants.
-From osiris.typing Require Import side stype.
 From osiris.encodings Require Import stype.
 From osiris.examples Require Import examples.