diff --git a/_CoqProject b/_CoqProject
index 2580fe31e32dbc0d4ded7616d52812d9342ad13b..388e1c6792f003b7f7cd9aec56c16854b2483023 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -85,6 +85,7 @@ 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/fixpoint.v
 theories/typing/examples/get_x.v
 theories/typing/examples/rebor.v
 theories/typing/examples/unbox.v
diff --git a/theories/typing/examples/fixpoint.v b/theories/typing/examples/fixpoint.v
new file mode 100644
index 0000000000000000000000000000000000000000..17b674c427dbb243aedd77b6dc035c53dcff006b
--- /dev/null
+++ b/theories/typing/examples/fixpoint.v
@@ -0,0 +1,20 @@
+From iris.proofmode Require Import proofmode.
+From lrust.typing Require Import typing.
+From iris.prelude Require Import options.
+
+Section fixpoint.
+  Context `{!typeGS Σ}.
+
+  Local Definition my_list_pre l : type := sum [ unit; box l].
+
+  Local Instance my_list_contractive : TypeContractive my_list_pre.
+  Proof.
+    (* FIXME: solve_type_proper should handle this. *)
+    intros n l1 l2 Hl. rewrite /my_list_pre.
+    f_equiv. constructor; last constructor; last by constructor.
+    - done.
+    - f_equiv. done.
+  Qed.
+
+  Definition my_list := type_fixpoint my_list_pre.
+End fixpoint.