diff --git a/prototyping/Luau/OpSem.agda b/prototyping/Luau/OpSem.agda
index 5abec889..c97cb973 100644
--- a/prototyping/Luau/OpSem.agda
+++ b/prototyping/Luau/OpSem.agda
@@ -62,10 +62,10 @@ data _⊢_⟶ᴱ_⊣_  where
     ---------------------------------
     H ⊢ (block b is done end) ⟶ᴱ nil ⊣ H
   
-  binOpEval : ∀ {H x op y} →
+  binOpEval : ∀ {H op} m n →
 
     --------------------------------------------------------------------------
-    H ⊢ (binexp (number x) op (number y)) ⟶ᴱ (number (evalBinOp x op y)) ⊣ H
+    H ⊢ (binexp (number m) op (number n)) ⟶ᴱ (number (evalBinOp m op n)) ⊣ H
   
   binOp₁ : ∀ {H H′ x x′ op y} →
 
diff --git a/prototyping/Luau/StrictMode.agda b/prototyping/Luau/StrictMode.agda
index 264ee37d..c89faf35 100644
--- a/prototyping/Luau/StrictMode.agda
+++ b/prototyping/Luau/StrictMode.agda
@@ -4,11 +4,11 @@ module Luau.StrictMode where
 
 open import Agda.Builtin.Equality using (_≡_)
 open import FFI.Data.Maybe using (just; nothing)
-open import Luau.Syntax using (Expr; Stat; Block; yes; nil; addr; var; var_∈_; _⟨_⟩∈_; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name)
-open import Luau.Type using (Type; strict; bot; top; nil; _⇒_; tgt)
+open import Luau.Syntax using (Expr; Stat; Block; yes; nil; addr; var; binexp; var_∈_; _⟨_⟩∈_; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name)
+open import Luau.Type using (Type; strict; bot; top; nil; number; _⇒_; tgt)
 open import Luau.Heap using (Heap; function_is_end) renaming (_[_] to _[_]ᴴ)
 open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_) renaming (_[_] to _[_]ⱽ)
-open import Luau.TypeCheck(strict) using (_⊢ᴮ_∈_; _⊢ᴱ_∈_; ⊢ᴴ_; ⊢ᴼ_; _⊢ᴴᴱ_▷_∈_; _⊢ᴴᴮ_▷_∈_; var; addr; app; block; return; local; function)
+open import Luau.TypeCheck(strict) using (_⊢ᴮ_∈_; _⊢ᴱ_∈_; ⊢ᴴ_; ⊢ᴼ_; _⊢ᴴᴱ_▷_∈_; _⊢ᴴᴮ_▷_∈_; var; addr; app; binexp; block; return; local; function)
 open import Properties.Equality using (_≢_)
 open import Properties.TypeCheck(strict) using (typeCheckᴮ)
 open import Properties.Product using (_,_)
@@ -51,6 +51,30 @@ data Warningᴱ H {Γ} where
     -----------------
     Warningᴱ H (app D₁ D₂)
 
+  BinopMismatch₁ : ∀ {op M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} →
+
+    (T ≢ number) →
+    ------------------------------
+    Warningᴱ H (binexp {op} D₁ D₂)
+
+  BinopMismatch₂ : ∀ {op M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} →
+
+    (U ≢ number) →
+    ------------------------------
+    Warningᴱ H (binexp {op} D₁ D₂)
+
+  bin₁ : ∀ {op M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} →
+
+    Warningᴱ H D₁ →    
+    ------------------------------
+    Warningᴱ H (binexp {op} D₁ D₂)
+
+  bin₂ : ∀ {op M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} →
+
+    Warningᴱ H D₂ →    
+    ------------------------------
+    Warningᴱ H (binexp {op} D₁ D₂)
+    
   function₀ : ∀ {f x B T U V} {D : (Γ ⊕ x ↦ T) ⊢ᴮ B ∈ V} →
 
     (U ≢ V) →
diff --git a/prototyping/Properties/Step.agda b/prototyping/Properties/Step.agda
index 9cb43f9e..348e6802 100644
--- a/prototyping/Properties/Step.agda
+++ b/prototyping/Properties/Step.agda
@@ -57,7 +57,7 @@ stepᴱ H (binexp M op N) with stepᴱ H M
 stepᴱ H (binexp M op N) | value v refl with stepᴱ H N
 stepᴱ H (binexp M op N) | value v refl | step H′ N′ s = step H′ (binexp (val v) op N′) (binOp₂ s)
 stepᴱ H (binexp M op N) | value v refl | error E = error (bin₂ E)
-stepᴱ H (binexp M op N) | value (number m) refl | value (number n) refl = step H (number (evalBinOp m op n)) binOpEval
+stepᴱ H (binexp M op N) | value (number m) refl | value (number n) refl = step H (number (evalBinOp m op n)) (binOpEval m n)
 stepᴱ H (binexp M op N) | value nil refl | value w refl = error (BinopMismatch₁ nil w λ ())
 stepᴱ H (binexp M op N) | value (addr a) refl | value w refl = error (BinopMismatch₁ (addr a) w λ ())
 stepᴱ H (binexp M op N) | value v refl | value nil refl = error (BinopMismatch₂ v nil (λ ()))
diff --git a/prototyping/Properties/StrictMode.agda b/prototyping/Properties/StrictMode.agda
index cf18663b..62e71d6c 100644
--- a/prototyping/Properties/StrictMode.agda
+++ b/prototyping/Properties/StrictMode.agda
@@ -6,7 +6,7 @@ import Agda.Builtin.Equality.Rewrite
 open import Agda.Builtin.Equality using (_≡_; refl)
 open import FFI.Data.Maybe using (Maybe; just; nothing)
 open import Luau.Heap using (Heap; Object; function_is_end; defn; alloc; ok; next; lookup-not-allocated) renaming (_≡_⊕_↦_ to _≡ᴴ_⊕_↦_; _[_] to _[_]ᴴ; ∅ to ∅ᴴ)
-open import Luau.StrictMode using (Warningᴱ; Warningᴮ; Warningᴼ; Warningᴴᴱ; Warningᴴᴮ; UnallocatedAddress; UnboundVariable; app₀; app₁; app₂; block₀; block₁; return; local₀; local₁; local₂; function₀; function₁; function₂; heap; expr; block; addr)
+open import Luau.StrictMode using (Warningᴱ; Warningᴮ; Warningᴼ; Warningᴴᴱ; Warningᴴᴮ; UnallocatedAddress; UnboundVariable; app₀; app₁; app₂; BinopMismatch₁; BinopMismatch₂; bin₁; bin₂; block₀; block₁; return; local₀; local₁; local₂; function₀; function₁; function₂; heap; expr; block; addr)
 open import Luau.Substitution using (_[_/_]ᴮ; _[_/_]ᴱ; _[_/_]ᴮunless_; var_[_/_]ᴱwhenever_)
 open import Luau.Syntax using (Expr; yes; var; var_∈_; _⟨_⟩∈_; _$_; addr; number; binexp; nil; function_is_end; block_is_end; done; return; local_←_; _∙_; fun; arg; name)
 open import Luau.Type using (Type; strict; nil; _⇒_; bot; tgt; _≡ᵀ_; _≡ᴹᵀ_)
@@ -20,7 +20,7 @@ open import Properties.Remember using (remember; _,_)
 open import Properties.Equality using (_≢_; sym; cong; trans; subst₁)
 open import Properties.Dec using (Dec; yes; no)
 open import Properties.Contradiction using (CONTRADICTION)
-open import Properties.TypeCheck(strict) using (typeOfᴼ; typeOfᴹᴼ; typeOfⱽ; typeOfᴱ; typeOfᴮ; typeOfᴱⱽ; typeCheckᴱ; typeCheckᴮ; typeCheckᴼ; typeCheckᴴᴱ; typeCheckᴴᴮ; mustBeFunction)
+open import Properties.TypeCheck(strict) using (typeOfᴼ; typeOfᴹᴼ; typeOfⱽ; typeOfᴱ; typeOfᴮ; typeOfᴱⱽ; typeCheckᴱ; typeCheckᴮ; typeCheckᴼ; typeCheckᴴᴱ; typeCheckᴴᴮ; mustBeFunction; mustBeNumber)
 open import Luau.OpSem using (_⊢_⟶*_⊣_; _⊢_⟶ᴮ_⊣_; _⊢_⟶ᴱ_⊣_; app₁; app₂; function; beta; return; block; done; local; subst; binOp₁; binOp₂; binOpEval; refl; step)
 open import Luau.RuntimeError using (RuntimeErrorᴱ; RuntimeErrorᴮ; FunctionMismatch; BinopMismatch₁; BinopMismatch₂; UnboundVariable; SEGV; app₁; app₂; bin₁; bin₂; block; local; return)
 
@@ -40,7 +40,7 @@ rednᴱ⊑ (beta O v p q) = refl
 rednᴱ⊑ (block s) = rednᴮ⊑ s
 rednᴱ⊑ (return v) = refl
 rednᴱ⊑ done = refl
-rednᴱ⊑ (binOpEval) = refl
+rednᴱ⊑ (binOpEval m n) = refl
 rednᴱ⊑ (binOp₁ s) = rednᴱ⊑ s
 rednᴱ⊑ (binOp₂ s) = rednᴱ⊑ s
 
@@ -168,7 +168,9 @@ preservationᴱ H (block var b ∈ T is return M ∙ B end) (return v) | no p =
 preservationᴱ H (block var b ∈ T is done end) (done) with T ≡ᵀ nil
 preservationᴱ H (block var b ∈ T is done end) (done) | yes p = ok p
 preservationᴱ H (block var b ∈ T is done end) (done) | no p = warning (expr (block₀ p))
-preservationᴱ H (binexp M op N) s = {!!}
+preservationᴱ H (binexp M op N) (binOpEval m n) = ok refl
+preservationᴱ H (binexp M op N) (binOp₁ s) = ok refl
+preservationᴱ H (binexp M op N) (binOp₂ s) = ok refl
 
 preservationᴮ H (local var x ∈ T ← M ∙ B) (local s) with heap-weakeningᴮ H B (rednᴱ⊑ s)
 preservationᴮ H (local var x ∈ T ← M ∙ B) (local s) | ok p = ok p
@@ -210,7 +212,10 @@ reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (
 reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (function₁ W) | no r = function₁ (reflect-substitutionᴮ-unless-no H B v x y r p (⊕-swap r) W)
 reflect-substitutionᴱ H (block var b ∈ T is B end) v x p (block₀ q) = block₀ (λ r → q (trans r (substitutivityᴮ H B v x p)))
 reflect-substitutionᴱ H (block var b ∈ T is B end) v x p (block₁ W) = block₁ (reflect-substitutionᴮ H B v x p W)
-reflect-substitutionᴱ H (binexp M op N) x v p W = {!!}
+reflect-substitutionᴱ H (binexp M op N) x v p (BinopMismatch₁ q) = BinopMismatch₁ (λ r → q (trans (sym (substitutivityᴱ H M x v p)) r))
+reflect-substitutionᴱ H (binexp M op N) x v p (BinopMismatch₂ q) = BinopMismatch₂ (λ r → q (trans (sym (substitutivityᴱ H N x v p)) r))
+reflect-substitutionᴱ H (binexp M op N) x v p (bin₁ W) = bin₁ (reflect-substitutionᴱ H M x v p W)
+reflect-substitutionᴱ H (binexp M op N) x v p (bin₂ W) = bin₂ (reflect-substitutionᴱ H N x v p W)
 
 reflect-substitutionᴱ-whenever-no H v x y p q (UnboundVariable y r) = UnboundVariable y (trans (sym (⊕-lookup-miss x y _ _ p)) r)
 reflect-substitutionᴱ-whenever-yes H (addr a) x x refl p (UnallocatedAddress q) with trans p (cong typeOfᴹᴼ q)
@@ -246,6 +251,14 @@ reflect-weakeningᴱ H (M $ N) h (app₀ p) | warning W | _ = app₁ W
 reflect-weakeningᴱ H (M $ N) h (app₀ p) | _ | warning W = app₂ W
 reflect-weakeningᴱ H (M $ N) h (app₁ W) = app₁ (reflect-weakeningᴱ H M h W)
 reflect-weakeningᴱ H (M $ N) h (app₂ W) = app₂ (reflect-weakeningᴱ H N h W)
+reflect-weakeningᴱ H (binexp M op N) h (BinopMismatch₁ p) with heap-weakeningᴱ H M h
+reflect-weakeningᴱ H (binexp M op N) h (BinopMismatch₁ p) | ok q = BinopMismatch₁ (λ r → p (trans (sym q) r))
+reflect-weakeningᴱ H (binexp M op N) h (BinopMismatch₁ p) | warning W = bin₁ W
+reflect-weakeningᴱ H (binexp M op N) h (BinopMismatch₂ p) with heap-weakeningᴱ H N h
+reflect-weakeningᴱ H (binexp M op N) h (BinopMismatch₂ p) | ok q = BinopMismatch₂ (λ r → p (trans (sym q) r))
+reflect-weakeningᴱ H (binexp M op N) h (BinopMismatch₂ p) | warning W = bin₂ W
+reflect-weakeningᴱ H (binexp M op N) h (bin₁ W′) = bin₁ (reflect-weakeningᴱ H M h W′)
+reflect-weakeningᴱ H (binexp M op N) h (bin₂ W′) = bin₂ (reflect-weakeningᴱ H N h W′)
 reflect-weakeningᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) h (function₀ p) with heap-weakeningᴮ H B h
 reflect-weakeningᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) h (function₀ p) | ok q = function₀ (λ r → p (trans r q))
 reflect-weakeningᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) h (function₀ p) | warning W = function₁ W
@@ -315,8 +328,30 @@ reflectᴱ H (block var b ∈ T is B end) (block s) (block₀ p) | warning (bloc
 reflectᴱ H (block var b ∈ T is B end) (block s) (block₁ W′) with reflectᴮ H B s W′
 reflectᴱ H (block var b ∈ T is B end) (block s) (block₁ W′) | heap W = heap W
 reflectᴱ H (block var b ∈ T is B end) (block s) (block₁ W′) | block W = expr (block₁ W)
+reflectᴱ H (block var b ∈ T is B end) (return v) W′ = expr (block₁ (return W′))
 reflectᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (UnallocatedAddress ())
-reflectᴱ H (block var b ∈ T is return M ∙ B end) (return v) W′ = expr (block₁ (return W′))
+reflectᴱ H (binexp M op N) (binOp₁ s) (BinopMismatch₁ p) with preservationᴱ H M s
+reflectᴱ H (binexp M op N) (binOp₁ s) (BinopMismatch₁ p) | ok q = expr (BinopMismatch₁ (λ r → p (trans (sym q) r)))
+reflectᴱ H (binexp M op N) (binOp₁ s) (BinopMismatch₁ p) | warning (heap W) = heap W
+reflectᴱ H (binexp M op N) (binOp₁ s) (BinopMismatch₁ p) | warning (expr W) = expr (bin₁ W)
+reflectᴱ H (binexp M op N) (binOp₁ s) (BinopMismatch₂ p) with heap-weakeningᴱ H N (rednᴱ⊑ s)
+reflectᴱ H (binexp M op N) (binOp₁ s) (BinopMismatch₂ p) | ok q = expr (BinopMismatch₂ (λ r → p (trans (sym q) r)))
+reflectᴱ H (binexp M op N) (binOp₁ s) (BinopMismatch₂ p) | warning W = expr (bin₂ W)
+reflectᴱ H (binexp M op N) (binOp₁ s) (bin₁ W′) with reflectᴱ H M s W′
+reflectᴱ H (binexp M op N) (binOp₁ s) (bin₁ W′) | heap W = heap W
+reflectᴱ H (binexp M op N) (binOp₁ s) (bin₁ W′) | expr W = expr (bin₁ W)
+reflectᴱ H (binexp M op N) (binOp₁ s) (bin₂ W′) = expr (bin₂ (reflect-weakeningᴱ H N (rednᴱ⊑ s) W′))
+reflectᴱ H (binexp M op N) (binOp₂ s) (BinopMismatch₁ p) with heap-weakeningᴱ H M (rednᴱ⊑ s)
+reflectᴱ H (binexp M op N) (binOp₂ s) (BinopMismatch₁ p) | ok q = expr (BinopMismatch₁ (λ r → p (trans (sym q) r)))
+reflectᴱ H (binexp M op N) (binOp₂ s) (BinopMismatch₁ p) | warning W = expr (bin₁ W)
+reflectᴱ H (binexp M op N) (binOp₂ s) (BinopMismatch₂ p) with preservationᴱ H N s
+reflectᴱ H (binexp M op N) (binOp₂ s) (BinopMismatch₂ p) | ok q = expr (BinopMismatch₂ (λ r → p (trans (sym q) r)))
+reflectᴱ H (binexp M op N) (binOp₂ s) (BinopMismatch₂ p) | warning (heap W) = heap W
+reflectᴱ H (binexp M op N) (binOp₂ s) (BinopMismatch₂ p) | warning (expr W) = expr (bin₂ W)
+reflectᴱ H (binexp M op N) (binOp₂ s) (bin₁ W′) = expr (bin₁ (reflect-weakeningᴱ H M (rednᴱ⊑ s) W′))
+reflectᴱ H (binexp M op N) (binOp₂ s) (bin₂ W′) with reflectᴱ H N s W′
+reflectᴱ H (binexp M op N) (binOp₂ s) (bin₂ W′) | heap W = heap W
+reflectᴱ H (binexp M op N) (binOp₂ s) (bin₂ W′) | expr W = expr (bin₂ W)
 
 reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (local₀ p) with preservationᴱ H M s
 reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (local₀ p) | ok q = block (local₀ (λ r → p (trans r q)))
@@ -360,7 +395,13 @@ reflectᴴᴱ H (block var b ∈ T is B end) (block s) (heap W′) | heap W = he
 reflectᴴᴱ H (block var b ∈ T is B end) (block s) (heap W′) | block W = expr (block₁ W)
 reflectᴴᴱ H (block var b ∈ T is return N ∙ B end) (return v) (heap W′) = heap W′
 reflectᴴᴱ H (block var b ∈ T is done end) done (heap W′) = heap W′
-reflectᴴᴱ H (binexp M op N) s W′ = {!!}
+reflectᴴᴱ H (binexp M op N) (binOpEval m n) (heap W′) = heap W′
+reflectᴴᴱ H (binexp M op N) (binOp₁ s) (heap W′) with reflectᴴᴱ H M s (heap W′)
+reflectᴴᴱ H (binexp M op N) (binOp₁ s) (heap W′) | heap W = heap W
+reflectᴴᴱ H (binexp M op N) (binOp₁ s) (heap W′) | expr W = expr (bin₁ W)
+reflectᴴᴱ H (binexp M op N) (binOp₂ s) (heap W′) with reflectᴴᴱ H N s (heap W′)
+reflectᴴᴱ H (binexp M op N) (binOp₂ s) (heap W′) | heap W = heap W
+reflectᴴᴱ H (binexp M op N) (binOp₂ s) (heap W′) | expr W = expr (bin₂ W)
 
 reflectᴴᴮ H B s (block W′) = reflectᴮ H B s W′
 reflectᴴᴮ H (local var x ∈ T ← M ∙ B) (local s) (heap W′) with reflectᴴᴱ H M s (heap W′)
@@ -392,10 +433,10 @@ runtimeWarningᴱ H (M $ N) (FunctionMismatch v w p) | warning W = app₂ W
 runtimeWarningᴱ H (M $ N) (app₁ err) = app₁ (runtimeWarningᴱ H M err)
 runtimeWarningᴱ H (M $ N) (app₂ err) = app₂ (runtimeWarningᴱ H N err)
 runtimeWarningᴱ H (block var b ∈ T is B end) (block err) = block₁ (runtimeWarningᴮ H B err)
-runtimeWarningᴱ H (binexp M op N) (BinopMismatch₁ v w p) = {!!}
-runtimeWarningᴱ H (binexp M op N) (BinopMismatch₂ v w p) = {!!}
-runtimeWarningᴱ H (binexp M op N) (bin₁ err) = {!bin₁!}
-runtimeWarningᴱ H (binexp M op N) (bin₂ err) = {!!}
+runtimeWarningᴱ H (binexp M op N) (BinopMismatch₁ v w p) = BinopMismatch₁ (λ q → p (mustBeNumber H ∅ v (sym q)))
+runtimeWarningᴱ H (binexp M op N) (BinopMismatch₂ v w p) = BinopMismatch₂ (λ q → p (mustBeNumber H ∅ w (sym q)))
+runtimeWarningᴱ H (binexp M op N) (bin₁ err) = bin₁ (runtimeWarningᴱ H M err)
+runtimeWarningᴱ H (binexp M op N) (bin₂ err) = bin₂ (runtimeWarningᴱ H N err)
 
 runtimeWarningᴮ H (local var x ∈ T ← M ∙ B) (local err) = local₁ (runtimeWarningᴱ H M err)
 runtimeWarningᴮ H (return M ∙ B) (return err) = return (runtimeWarningᴱ H M err)
diff --git a/prototyping/Properties/TypeCheck.agda b/prototyping/Properties/TypeCheck.agda
index 3384fc52..04f58e67 100644
--- a/prototyping/Properties/TypeCheck.agda
+++ b/prototyping/Properties/TypeCheck.agda
@@ -64,6 +64,15 @@ mustBeFunction H Γ nil p = CONTRADICTION (p refl)
 mustBeFunction H Γ (addr a) p = refl
 mustBeFunction H Γ (number n) p = CONTRADICTION (p refl)
 
+mustBeNumber : ∀ H Γ v → (number ≡ typeOfᴱ H Γ (val v)) → (number ≡ valueType(v))
+mustBeNumber H Γ nil ()
+mustBeNumber H Γ (addr a) p with remember (H [ a ]ᴴ)
+mustBeNumber H Γ (addr a) p | (just O , q) with trans p (cong orBot (cong typeOfᴹᴼ q))
+mustBeNumber H Γ (addr a) p | (just function f ⟨ var x ∈ T ⟩∈ U is B end , q) | ()
+mustBeNumber H Γ (addr a) p | (nothing , q) with trans p (cong orBot (cong typeOfᴹᴼ q))
+mustBeNumber H Γ (addr a) p | nothing , q | ()
+mustBeNumber H Γ (number n) p = refl
+
 typeCheckᴱ : ∀ H Γ M → (Γ ⊢ᴱ M ∈ (typeOfᴱ H Γ M))
 typeCheckᴮ : ∀ H Γ B → (Γ ⊢ᴮ B ∈ (typeOfᴮ H Γ B))