diff --git a/Veir/IR/WellFormed.lean b/Veir/IR/WellFormed.lean
index fb03a5f..7dca59d 100644
--- a/Veir/IR/WellFormed.lean
+++ b/Veir/IR/WellFormed.lean
@@ -589,6 +589,8 @@ attribute [grind →] RegionPtr.BlockChain.inBounds
 structure Operation.WellFormed (op : Operation) (ctx : IRContext) (opPtr : OperationPtr) hop : Prop where
   inBounds : Operation.FieldsInBounds opPtr ctx hop
   result_index i (iInBounds : i < opPtr.getNumResults! ctx) : ((opPtr.getResult i).get! ctx).index = i
+  result_owner i (iInBounds : i < opPtr.getNumResults! ctx) :
+    ((opPtr.getResult i).get! ctx).owner = opPtr
   operand_owner i (iInBounds : i < opPtr.getNumOperands! ctx) : ((opPtr.getOpOperand i).get! ctx).owner = opPtr
   blockOperand_owner i (iInBounds : i < opPtr.getNumSuccessors! ctx) : ((opPtr.getBlockOperand i).get! ctx).owner = opPtr
   regions_unique i (iInBounds : i < opPtr.getNumRegions! ctx) j (jInBounds : j < opPtr.getNumRegions! ctx) :
@@ -729,6 +731,9 @@ theorem Operation.WellFormed_unchanged
     (hSameResultIndex :
       ∀ i, i < opPtr.getNumResults ctx opPtrInBounds →
       ((opPtr.getResult i).get! ctx).index = ((opPtr.getResult i).get! ctx').index)
+    (hSameResultOwner :
+      ∀ i, i < opPtr.getNumResults ctx opPtrInBounds →
+      ((opPtr.getResult i).get! ctx).owner = ((opPtr.getResult i).get! ctx').owner)
     (hSameRegionParents :
       ∀ (regionPtr : RegionPtr), regionPtr.InBounds ctx →
         (regionPtr.get! ctx).parent = some opPtr →
diff --git a/Veir/Rewriter/WellFormed/Builder/OpOperands.lean b/Veir/Rewriter/WellFormed/Builder/OpOperands.lean
index eba9d26..065d165 100644
--- a/Veir/Rewriter/WellFormed/Builder/OpOperands.lean
+++ b/Veir/Rewriter/WellFormed/Builder/OpOperands.lean
@@ -342,7 +342,7 @@ theorem Rewriter.pushOperand_WellFormed  (valuePtr : ValuePtr) (valuePtrInBounds
         pushOperand_OperationPtr_get_next_mono, pushOperand_BlockPtr_get_lastOp_mono, pushOperand_BlockPtr_get_firstOp_mono]
   case operations =>
     intros opPtr' opPtrInBounds
-    have ⟨h₁, h₂, h₃, h₄, h₅, h₆⟩ := hOpWf.operations opPtr' (by grind)
+    have ⟨h₁, h₂, h₃, h₄, h₅, h₆, h₇⟩ := hOpWf.operations opPtr' (by grind)
     constructor
     case region_parent =>
       intros region regionInBounds
diff --git a/Veir/Rewriter/WellFormed/Builder/OpResults.lean b/Veir/Rewriter/WellFormed/Builder/OpResults.lean
index bfb560c..0886961 100644
--- a/Veir/Rewriter/WellFormed/Builder/OpResults.lean
+++ b/Veir/Rewriter/WellFormed/Builder/OpResults.lean
@@ -9,7 +9,8 @@ theorem Rewriter.pushResult_WellFormed (ctx: IRContext) (opPtr: OperationPtr)
     (hop : opPtr.InBounds ctx) (hctx : IRContext.WellFormed ctx)
     (hres : newResult.FieldsInBounds (opPtr.pushResult ctx newResult hop))
     (hNoFirst : newResult.firstUse = none)
-    (hIndex : newResult.index = opPtr.getNumResults ctx) :
+    (hIndex : newResult.index = opPtr.getNumResults ctx)
+    (hOwner : newResult.owner = opPtr) :
     (opPtr.pushResult ctx newResult hop).WellFormed := by
   have ⟨h₁, h₂, h₃, h₄, h₅, h₆, h₇, h₈⟩ := hctx
   constructor
@@ -43,7 +44,7 @@ theorem Rewriter.pushResult_WellFormed (ctx: IRContext) (opPtr: OperationPtr)
   case operations =>
     intros op hop
     have : op.InBounds ctx := by grind
-    have ⟨ha, hb, hc, hd, he, hf⟩ := h₆ op this
+    have ⟨ha, hb, hc, hd, he, hf, hg⟩ := h₆ op this
     constructor
     -- TODO: Understand why grind fails here
     case region_parent => intros; constructor <;> simp <;> grind
diff --git a/Veir/Rewriter/WellFormed/Rewriter/Operation.lean b/Veir/Rewriter/WellFormed/Rewriter/Operation.lean
index e23ed03..668b7ed 100644
--- a/Veir/Rewriter/WellFormed/Rewriter/Operation.lean
+++ b/Veir/Rewriter/WellFormed/Rewriter/Operation.lean
@@ -53,7 +53,7 @@ theorem Rewriter.insertOp?_WellFormed (ctx : IRContext) (hctx : ctx.WellFormed)
   case operations =>
     intros op hop
     have : op.InBounds ctx := by grind
-    have ⟨ha, hb, hc, hd, he, hf⟩ := h₆ op this
+    have ⟨ha, hb, hc, hd, he, hf, hg⟩ := h₆ op this
     apply Operation.WellFormed_unchanged (ctx := ctx) <;> grind
   case blocks =>
     intros bl hbl
@@ -159,7 +159,7 @@ theorem Rewriter.detachOp_WellFormed (ctx : IRContext) (wf : ctx.WellFormed)
   case operations =>
     intros op' hop'
     have : op'.InBounds ctx := by grind
-    have ⟨ha, hb, hc, hd, he, hf⟩ := h₆ op' this
+    have ⟨ha, hb, hc, hd, he, hf, hg⟩ := h₆ op' this
     apply Operation.WellFormed_unchanged (ctx := ctx) <;> grind
   case blocks =>
     intros bl hbl