diff --git a/lean/Spa/Language/Base.lean b/lean/Spa/Language/Base.lean
index 1228cc3..78e68b7 100644
--- a/lean/Spa/Language/Base.lean
+++ b/lean/Spa/Language/Base.lean
@@ -21,17 +21,6 @@ inductive Stmt where
   | whileLoop (e : Expr) (s : Stmt)
   deriving DecidableEq
 
-inductive Expr.HasVar : String → Expr → Prop
-  | addLeft {e₁ e₂ k} : Expr.HasVar k e₁ → Expr.HasVar k (.add e₁ e₂)
-  | addRight {e₁ e₂ k} : Expr.HasVar k e₂ → Expr.HasVar k (.add e₁ e₂)
-  | subLeft {e₁ e₂ k} : Expr.HasVar k e₁ → Expr.HasVar k (.sub e₁ e₂)
-  | subRight {e₁ e₂ k} : Expr.HasVar k e₂ → Expr.HasVar k (.sub e₁ e₂)
-  | here {k} : Expr.HasVar k (.var k)
-
-inductive BasicStmt.HasVar : String → BasicStmt → Prop
-  | assignLeft {k e} : BasicStmt.HasVar k (.assign k e)
-  | assignRight {k k' e} : Expr.HasVar k e → BasicStmt.HasVar k (.assign k' e)
-
 def Expr.vars : Expr → Finset String
   | .add l r => l.vars ∪ r.vars
   | .sub l r => l.vars ∪ r.vars
@@ -48,7 +37,4 @@ def Stmt.vars : Stmt → Finset String
   | .ifElse e s₁ s₂ => (e.vars ∪ s₁.vars) ∪ s₂.vars
   | .whileLoop e s => e.vars ∪ s.vars
 
-def Stmt.varsList (ss : List Stmt) : Finset String :=
-  ss.foldr (fun s acc => s.vars ∪ acc) ∅
-
 end Spa