diff --git a/formalizations/guarded-cubical/Syntax/SyntacticBisimilarity.agda b/formalizations/guarded-cubical/Syntax/SyntacticBisimilarity.agda
index b391130c3c1c2354e325faf394abbd5b2ea73f9c..37ad5d56400262cc9cea23bebdadfe09325ac59e 100644
--- a/formalizations/guarded-cubical/Syntax/SyntacticBisimilarity.agda
+++ b/formalizations/guarded-cubical/Syntax/SyntacticBisimilarity.agda
@@ -1,3 +1,4 @@
+{-# OPTIONS --allow-unsolved-metas #-}
 
 module Syntax.SyntacticBisimilarity where
 
@@ -217,4 +218,5 @@ _≈->>_ M≈M' N≈N' = ≈-plugE (≈-bind N≈N') M≈M'
 ≈v-refl (isSetVal V V₁ x y i i₁) = {!!}
 ≈v-refl (isPosetVal x x₁ i) = {!!}
   
+
 -}