diff --git a/prototyping/Luau/OpSem.agda b/prototyping/Luau/OpSem.agda
index 493a5e22..cbb55978 100644
--- a/prototyping/Luau/OpSem.agda
+++ b/prototyping/Luau/OpSem.agda
@@ -23,12 +23,8 @@ evalEqOp (bool false) (bool y) = not y
 evalEqOp _ _ = false
 
 evalNeqOp : Value → Value → Bool
-evalNeqOp Value.nil Value.nil = false
-evalNeqOp (addr x) (addr y) = not (x ==ᴬ y)
 evalNeqOp (number x) (number y) = primFloatInequality x y
-evalNeqOp (bool true) (bool y) = not y
-evalNeqOp (bool false) (bool y) = y
-evalNeqOp _ _ = true
+evalNeqOp x y = not (evalEqOp x y)
 
 data _⟦_⟧_⟶_ : Value → BinaryOperator → Value → Value → Set where
   + : ∀ m n → (number m) ⟦ + ⟧ (number n) ⟶ number (primFloatPlus m n)
diff --git a/prototyping/Luau/VarCtxt.agda b/prototyping/Luau/VarCtxt.agda
index a9280ec4..76f64dfe 100644
--- a/prototyping/Luau/VarCtxt.agda
+++ b/prototyping/Luau/VarCtxt.agda
@@ -22,7 +22,7 @@ _⋓_ : VarCtxt → VarCtxt → VarCtxt
 _⋓_ = unionWith _∪_
 
 _[_] : VarCtxt → Var → Maybe Type
-_[_] Γ x = lookup (fromString x) Γ
+Γ [ x ] = lookup (fromString x) Γ
 
 _⊝_ : VarCtxt → Var → VarCtxt
 Γ ⊝ x = delete (fromString x) Γ