diff --git a/Veir/ForLean.lean b/Veir/ForLean.lean
index 91d9e49..906d76e 100644
--- a/Veir/ForLean.lean
+++ b/Veir/ForLean.lean
@@ -1,5 +1,7 @@
 module
 
+public import Std.Data.ExtHashSet
+
 public section
 
 /-- Checks if a UInt8 character is an alphabetic character or underscore in UTF-8. -/
@@ -115,6 +117,11 @@ theorem Nat.eq_iff_forall_lessthan :
 
 deriving instance DecidableEq for Except
 
+@[simp, grind =]
+theorem Std.ExtHashSet.filter_empty {α : Type} [Hashable α] [BEq α] [LawfulBEq α] (f : α → Bool) :
+    (∅ : Std.ExtHashSet α).filter f = ∅ := by
+  grind
+
 section ranges
 
 open Std
diff --git a/Veir/IR/WellFormed.lean b/Veir/IR/WellFormed.lean
index 90efae9..fb03a5f 100644
--- a/Veir/IR/WellFormed.lean
+++ b/Veir/IR/WellFormed.lean
@@ -606,12 +606,14 @@ structure Region.WellFormed (region : Region) (ctx : IRContext) (regionPtr : Reg
   inBounds : region.FieldsInBounds ctx
   parent_op {op} (heq : region.parent = some op) : ∃ i, i < op.getNumRegions! ctx → op.getRegion! ctx i = regionPtr
 
-structure IRContext.WellFormed (ctx : IRContext) : Prop where
+structure IRContext.WellFormed (ctx : IRContext)
+  (missingOperandUses : Std.ExtHashSet OpOperandPtr := ∅)
+  (missingSuccessorUses : Std.ExtHashSet BlockOperandPtr := ∅) : Prop where
   inBounds : ctx.FieldsInBounds
   valueDefUseChains (valuePtr : ValuePtr) (valuePtrInBounds : valuePtr.InBounds ctx) :
-    ∃ array, ValuePtr.DefUse valuePtr ctx array
+    ∃ array, ValuePtr.DefUse valuePtr ctx array (missingOperandUses.filter (fun use => (use.get! ctx).value = valuePtr))
   blockDefUseChains (blockPtr : BlockPtr) (blockPtrInBounds : blockPtr.InBounds ctx) :
-    ∃ array, BlockPtr.DefUse blockPtr ctx array
+    ∃ array, BlockPtr.DefUse blockPtr ctx array (missingSuccessorUses.filter (fun use => (use.get! ctx).value = blockPtr))
   opChain (blockPtr : BlockPtr) (blockPtrInBounds : blockPtr.InBounds ctx) :
     ∃ array, BlockPtr.OpChain blockPtr ctx array
   blockChain (regionPtr : RegionPtr) (regionPtrInBounds : regionPtr.InBounds ctx) :
@@ -792,8 +794,8 @@ noncomputable def ValuePtr.defUseArray (value : ValuePtr) (ctx : IRContext) (hct
 
 @[grind .]
 theorem ValuePtr.defUseArrayWF {hctx : IRContext.WellFormed ctx} :
-    ValuePtr.DefUse value ctx (ValuePtr.defUseArray value ctx hctx hvalue) :=
-  Exists.choose_spec (hctx.valueDefUseChains value hvalue)
+    ValuePtr.DefUse value ctx (ValuePtr.defUseArray value ctx hctx hvalue) := by
+  grind [ValuePtr.defUseArray]
 
 theorem ValuePtr.defUseArray_contains_operand_use :
     (operand.get ctx operandInBounds).value = value ↔
diff --git a/Veir/Rewriter/WellFormed/Rewriter/Value.lean b/Veir/Rewriter/WellFormed/Rewriter/Value.lean
index 633a75c..79496ec 100644
--- a/Veir/Rewriter/WellFormed/Rewriter/Value.lean
+++ b/Veir/Rewriter/WellFormed/Rewriter/Value.lean
@@ -112,6 +112,7 @@ theorem Rewriter.replaceUse_WellFormed (ctx: IRContext) (use : OpOperandPtr) (ne
       have ⟨array, harray⟩ := hWf.valueDefUseChains value (by grind)
       have ⟨newArray, hnewArray⟩ := hWf.valueDefUseChains newValue (by grind)
       have ⟨array', hArray'⟩ := hWf.valueDefUseChains valuePtr (by grind)
+      simp only [Std.ExtHashSet.filter_empty]
       apply Rewriter.replaceUse_DefUse
         (value := value) (array := array) (array' := newArray) (array'' := array') <;> grind
     case blockDefUseChains =>