diff --git a/theories/typing/lib/option.v b/theories/typing/lib/option.v
index b7d0b2fd5ed038782bf65f517db52866c20dafd3..4a1a153e61804ea31cdf73ac51eecf361644df81 100644
--- a/theories/typing/lib/option.v
+++ b/theories/typing/lib/option.v
@@ -7,6 +7,12 @@ Section option.
 
   Definition option (τ : type) := Σ[unit; τ]%T.
 
+  Global Instance option_ne : NonExpansive option.
+  Proof. solve_proper. Qed.
+
+  Global Instance option_type_ne : TypeNonExpansive option.
+  Proof. solve_proper. Qed.
+
   (* Variant indices. *)
   Definition none := 0%nat.
   Definition some := 1%nat.