diff --git a/prototyping/Examples/Run.agda b/prototyping/Examples/Run.agda
index 60f437f8..70863cc9 100644
--- a/prototyping/Examples/Run.agda
+++ b/prototyping/Examples/Run.agda
@@ -1,5 +1,4 @@
 {-# OPTIONS --rewriting #-}
-{-# OPTIONS --allow-unsolved-metas #-}
 
 module Examples.Run where
 
@@ -9,10 +8,10 @@ open import Luau.Value using (nil; number)
 open import Luau.Run using (run; return)
 
 ex1 : (run (function "id" ⟨ var "x" ⟩ is return (var "x") ∙ done end ∙ return (var "id" $ nil) ∙ done) ≡ return nil _)
-ex1 = {!!}
+ex1 = refl
 
 ex2 : (run (function "fn" ⟨ var "x" ⟩ is return (number 123.0) ∙ done end ∙ return (var "fn" $ nil) ∙ done) ≡ return (number 123.0) _)
-ex2 = {!!}
+ex2 = refl
 
 ex3 : (run (function "fn" ⟨ var "x" ⟩ is return (binexp (number 1.0) + (number 2.0)) ∙ done end ∙ return (var "fn" $ nil) ∙ done) ≡ return (number 3.0) _)
-ex3 = {!!}
+ex3 = refl