diff --git a/prototyping/Properties/Subtyping.agda b/prototyping/Properties/Subtyping.agda
index 4c1be220..4225491b 100644
--- a/prototyping/Properties/Subtyping.agda
+++ b/prototyping/Properties/Subtyping.agda
@@ -1,5 +1,5 @@
 {-# OPTIONS --rewriting #-}
-{-# OPTIONS --allow-unsolved-metas #-}
+
 module Properties.Subtyping where
 
 open import Agda.Builtin.Equality using (_≡_; refl)