diff --git a/_CoqProject b/_CoqProject
index c2110fe31770d3d7c04fb3596e9fbc3706bb59ea..411cae53bc79aa3f6351c928859fca2ada348d14 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -45,22 +45,22 @@ theories/typing/fixpoint.v
 theories/typing/type_sum.v
 theories/typing/typing.v
 theories/typing/soundness.v
-theories/typing/option.v
-theories/typing/unsafe/fake_shared_box.v
-theories/typing/unsafe/cell.v
-theories/typing/unsafe/spawn.v
-theories/typing/unsafe/refcell/refcell.v
-theories/typing/unsafe/refcell/ref.v
-theories/typing/unsafe/refcell/refmut.v
-theories/typing/unsafe/refcell/refcell_code.v
-theories/typing/unsafe/refcell/ref_code.v
-theories/typing/unsafe/refcell/refmut_code.v
-theories/typing/unsafe/rwlock/rwlock.v
-theories/typing/unsafe/rwlock/rwlockreadguard.v
-theories/typing/unsafe/rwlock/rwlockwriteguard.v
-theories/typing/unsafe/rwlock/rwlock_code.v
-theories/typing/unsafe/rwlock/rwlockreadguard_code.v
-theories/typing/unsafe/rwlock/rwlockwriteguard_code.v
+theories/typing/lib/option.v
+theories/typing/lib/fake_shared_box.v
+theories/typing/lib/cell.v
+theories/typing/lib/spawn.v
+theories/typing/lib/refcell/refcell.v
+theories/typing/lib/refcell/ref.v
+theories/typing/lib/refcell/refmut.v
+theories/typing/lib/refcell/refcell_code.v
+theories/typing/lib/refcell/ref_code.v
+theories/typing/lib/refcell/refmut_code.v
+theories/typing/lib/rwlock/rwlock.v
+theories/typing/lib/rwlock/rwlockreadguard.v
+theories/typing/lib/rwlock/rwlockwriteguard.v
+theories/typing/lib/rwlock/rwlock_code.v
+theories/typing/lib/rwlock/rwlockreadguard_code.v
+theories/typing/lib/rwlock/rwlockwriteguard_code.v
 theories/typing/examples/get_x.v
 theories/typing/examples/rebor.v
 theories/typing/examples/unbox.v
diff --git a/theories/typing/unsafe/cell.v b/theories/typing/lib/cell.v
similarity index 100%
rename from theories/typing/unsafe/cell.v
rename to theories/typing/lib/cell.v
diff --git a/theories/typing/unsafe/fake_shared_box.v b/theories/typing/lib/fake_shared_box.v
similarity index 100%
rename from theories/typing/unsafe/fake_shared_box.v
rename to theories/typing/lib/fake_shared_box.v
diff --git a/theories/typing/option.v b/theories/typing/lib/option.v
similarity index 100%
rename from theories/typing/option.v
rename to theories/typing/lib/option.v
diff --git a/theories/typing/unsafe/refcell/ref.v b/theories/typing/lib/refcell/ref.v
similarity index 98%
rename from theories/typing/unsafe/refcell/ref.v
rename to theories/typing/lib/refcell/ref.v
index c9c8b761a4cb361e1f4f44258656a9f2c8461db2..9fe6e746df7a57d49015b129963d21c956123759 100644
--- a/theories/typing/unsafe/refcell/ref.v
+++ b/theories/typing/lib/refcell/ref.v
@@ -3,7 +3,7 @@ From iris.algebra Require Import auth csum frac agree.
 From iris.base_logic Require Import big_op fractional.
 From lrust.lifetime Require Import na_borrow.
 From lrust.typing Require Import typing.
-From lrust.typing.unsafe.refcell Require Import refcell.
+From lrust.typing.lib.refcell Require Import refcell.
 Set Default Proof Using "Type".
 
 Definition refcell_refN := refcellN .@ "ref".
diff --git a/theories/typing/unsafe/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
similarity index 99%
rename from theories/typing/unsafe/refcell/ref_code.v
rename to theories/typing/lib/refcell/ref_code.v
index 8028c93efcdb6999e6d8c3ceaf0690304d9a2e2e..e2858d9359a39e60df0553583f85bc11f7718334 100644
--- a/theories/typing/unsafe/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -4,7 +4,7 @@ From iris.algebra Require Import auth csum frac agree.
 From iris.base_logic Require Import big_op fractional.
 From lrust.lifetime Require Import lifetime na_borrow.
 From lrust.typing Require Import typing.
-From lrust.typing.unsafe.refcell Require Import refcell ref.
+From lrust.typing.lib.refcell Require Import refcell ref.
 Set Default Proof Using "Type".
 
 Section ref_functions.
diff --git a/theories/typing/unsafe/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
similarity index 100%
rename from theories/typing/unsafe/refcell/refcell.v
rename to theories/typing/lib/refcell/refcell.v
diff --git a/theories/typing/unsafe/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
similarity index 99%
rename from theories/typing/unsafe/refcell/refcell_code.v
rename to theories/typing/lib/refcell/refcell_code.v
index af0545bc2e7b5ea949709e9b3f1b89366ccd13b1..d807fb209e78c4ec6f2a3bf6c5cafea4a587c043 100644
--- a/theories/typing/unsafe/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -5,7 +5,7 @@ From iris.base_logic Require Import big_op fractional.
 From lrust.lang Require Import memcpy.
 From lrust.lifetime Require Import na_borrow.
 From lrust.typing Require Import typing option.
-From lrust.typing.unsafe.refcell Require Import refcell ref refmut.
+From lrust.typing.lib.refcell Require Import refcell ref refmut.
 Set Default Proof Using "Type".
 
 Section refcell_functions.
diff --git a/theories/typing/unsafe/refcell/refmut.v b/theories/typing/lib/refcell/refmut.v
similarity index 99%
rename from theories/typing/unsafe/refcell/refmut.v
rename to theories/typing/lib/refcell/refmut.v
index 2dbaf8465e5aa49de9018d724c02c887e487a900..bc9e076c94dd1cbde4ff947d818b54d47cf5355c 100644
--- a/theories/typing/unsafe/refcell/refmut.v
+++ b/theories/typing/lib/refcell/refmut.v
@@ -3,7 +3,7 @@ From iris.algebra Require Import auth csum frac agree.
 From iris.base_logic Require Import big_op fractional.
 From lrust.lifetime Require Import na_borrow.
 From lrust.typing Require Import typing.
-From lrust.typing.unsafe.refcell Require Import refcell.
+From lrust.typing.lib.refcell Require Import refcell.
 Set Default Proof Using "Type".
 
 Section refmut.
diff --git a/theories/typing/unsafe/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
similarity index 99%
rename from theories/typing/unsafe/refcell/refmut_code.v
rename to theories/typing/lib/refcell/refmut_code.v
index d4b0c140c5659c06a72a64d471c0d23cc7a3753a..b0c55bedc7514eaf7204bfd00d1530865a5294cc 100644
--- a/theories/typing/unsafe/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -4,7 +4,7 @@ From iris.algebra Require Import auth csum frac agree.
 From iris.base_logic Require Import big_op fractional.
 From lrust.lifetime Require Import na_borrow.
 From lrust.typing Require Import typing.
-From lrust.typing.unsafe.refcell Require Import refcell refmut.
+From lrust.typing.lib.refcell Require Import refcell refmut.
 Set Default Proof Using "Type".
 
 Section refmut_functions.
diff --git a/theories/typing/unsafe/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
similarity index 100%
rename from theories/typing/unsafe/rwlock/rwlock.v
rename to theories/typing/lib/rwlock/rwlock.v
diff --git a/theories/typing/unsafe/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
similarity index 99%
rename from theories/typing/unsafe/rwlock/rwlock_code.v
rename to theories/typing/lib/rwlock/rwlock_code.v
index f077e07228dd8038c8016b61f65e09a25f56d46b..bb3f04008457d83d24e8a4b46321cd282e26fdbe 100644
--- a/theories/typing/unsafe/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -5,7 +5,7 @@ From iris.base_logic Require Import big_op fractional.
 From lrust.lang Require Import memcpy.
 From lrust.lifetime Require Import na_borrow.
 From lrust.typing Require Import typing option.
-From lrust.typing.unsafe.rwlock Require Import rwlock rwlockreadguard rwlockwriteguard.
+From lrust.typing.lib.rwlock Require Import rwlock rwlockreadguard rwlockwriteguard.
 Set Default Proof Using "Type".
 
 Section rwlock_functions.
diff --git a/theories/typing/unsafe/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
similarity index 98%
rename from theories/typing/unsafe/rwlock/rwlockreadguard.v
rename to theories/typing/lib/rwlock/rwlockreadguard.v
index 01076b7a99cfa049151112c86ae3443dc2475167..6a61a4adfb58401b16dc58c96b658ae69d2f47a4 100644
--- a/theories/typing/unsafe/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -3,7 +3,7 @@ From iris.algebra Require Import auth csum frac agree.
 From iris.base_logic Require Import big_op fractional.
 From lrust.lifetime Require Import na_borrow.
 From lrust.typing Require Import typing.
-From lrust.typing.unsafe.rwlock Require Import rwlock.
+From lrust.typing.lib.rwlock Require Import rwlock.
 Set Default Proof Using "Type".
 
 Section rwlockreadguard.
diff --git a/theories/typing/unsafe/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
similarity index 99%
rename from theories/typing/unsafe/rwlock/rwlockreadguard_code.v
rename to theories/typing/lib/rwlock/rwlockreadguard_code.v
index 786d1abb82b91bf4156001d2ed2156e08a630dd3..12ececef0f687202b63dbe1847280ad196c85e24 100644
--- a/theories/typing/unsafe/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -4,7 +4,7 @@ From iris.algebra Require Import auth csum frac agree.
 From iris.base_logic Require Import big_op fractional.
 From lrust.lifetime Require Import lifetime na_borrow.
 From lrust.typing Require Import typing.
-From lrust.typing.unsafe.rwlock Require Import rwlock rwlockreadguard.
+From lrust.typing.lib.rwlock Require Import rwlock rwlockreadguard.
 Set Default Proof Using "Type".
 
 Section rwlockreadguard_functions.
diff --git a/theories/typing/unsafe/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
similarity index 99%
rename from theories/typing/unsafe/rwlock/rwlockwriteguard.v
rename to theories/typing/lib/rwlock/rwlockwriteguard.v
index 660d3fd955aafd81d2154b4f665773d0f9fc97ec..ac8397324fa5f678bb4c09b0609245ad3cc3c034 100644
--- a/theories/typing/unsafe/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -3,7 +3,7 @@ From iris.algebra Require Import auth csum frac agree.
 From iris.base_logic Require Import big_op fractional.
 From lrust.lifetime Require Import na_borrow.
 From lrust.typing Require Import typing.
-From lrust.typing.unsafe.rwlock Require Import rwlock.
+From lrust.typing.lib.rwlock Require Import rwlock.
 Set Default Proof Using "Type".
 
 Section rwlockwriteguard.
diff --git a/theories/typing/unsafe/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
similarity index 99%
rename from theories/typing/unsafe/rwlock/rwlockwriteguard_code.v
rename to theories/typing/lib/rwlock/rwlockwriteguard_code.v
index 4cf42859f0a36baad5b30ddc51040fad8d1a61f0..620771766340a8c965323346c3152002836c9597 100644
--- a/theories/typing/unsafe/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -4,7 +4,7 @@ From iris.algebra Require Import auth csum frac agree.
 From iris.base_logic Require Import big_op fractional.
 From lrust.lifetime Require Import na_borrow.
 From lrust.typing Require Import typing.
-From lrust.typing.unsafe.rwlock Require Import rwlock rwlockwriteguard.
+From lrust.typing.lib.rwlock Require Import rwlock rwlockwriteguard.
 Set Default Proof Using "Type".
 
 Section rwlockwriteguard_functions.
diff --git a/theories/typing/unsafe/spawn.v b/theories/typing/lib/spawn.v
similarity index 100%
rename from theories/typing/unsafe/spawn.v
rename to theories/typing/lib/spawn.v