diff --git a/Arm/Memory/Common.lean b/Arm/Memory/Common.lean
index 544fb4cb..8ba58452 100644
--- a/Arm/Memory/Common.lean
+++ b/Arm/Memory/Common.lean
@@ -227,6 +227,9 @@ inductive Hypothesis
 | pairwiseSeparate (proof : MemPairwiseSeparateProof e)
 | read_eq (proof : ReadBytesEqProof)
 
+def Hypothesis.isPairwiseSeparate : Hypothesis → Bool
+| .pairwiseSeparate _ => true
+| _ => false
 
 def Hypothesis.proof : Hypothesis → Expr
 | .pairwiseSeparate proof  => proof.h
@@ -245,17 +248,35 @@ instance : ToMessageData Hypothesis where
 
 /-- create a trace node in trace class (i.e. `set_option traceClass true`),
 with header `header`, whose default collapsed state is `collapsed`. -/
-def TacticM.withTraceNode' (header : MessageData) (k : TacticM α)
+def TacticM.withTraceNode'
+    [Monad m]
+    [MonadTrace m]
+    [MonadLiftT IO m]
+    [MonadRef m]
+    [AddMessageContext m]
+    [MonadOptions m]
+    [always : MonadAlwaysExcept ε m]
+    [MonadLiftT BaseIO m]
+    (header : MessageData) (k : m α)
     (collapsed : Bool := false)
-    (traceClass : Name := `simp_mem.info) : TacticM α :=
+    (traceClass : Name := `simp_mem.info) : m α :=
   Lean.withTraceNode traceClass (fun _ => return header) k (collapsed := collapsed)
 
 /-- Create a trace note that folds `header` with `(NOTE: can be large)`,
 and prints `msg` under such a trace node. Collapsed by default.
 -/
-def TacticM.traceLargeMsg (header : MessageData) (msg : MessageData) : TacticM Unit := do
+def TacticM.traceLargeMsg
+    [Monad m]
+    [MonadTrace m]
+    [MonadLiftT IO m]
+    [MonadRef m]
+    [AddMessageContext m]
+    [MonadOptions m]
+    [always : MonadAlwaysExcept ε m]
+    [MonadLiftT BaseIO m]
+    (header : MessageData)
+    (msg : MessageData) : m Unit := do
     withTraceNode' m!"{header} (NOTE: can be large)" (collapsed := true) do
-      -- | TODO: change trace class?
       trace[simp_mem.info] msg
 
 
@@ -270,7 +291,7 @@ def omega (bvToNatSimpCtx : Simp.Context) (bvToNatSimprocs : Array Simp.Simprocs
       trace[simp_mem.info] "{goal}"
     -- @bollu: TODO: understand what precisely we are recovering from.
     withoutRecover do
-    evalTactic (← `(tactic| bv_omega_bench))
+      evalTactic (← `(tactic| bv_omega_bench))
 
 /-
 Introduce a new definition into the local context, simplify it using `simp`,
@@ -278,7 +299,6 @@ and return the FVarId of the new definition in the goal.
 -/
 def simpAndIntroDef (name : String) (hdefVal : Expr) : TacticM FVarId  := do
   withMainContext do
-
     let name ← mkFreshUserName <| .mkSimple name
     let goal ← getMainGoal
     let hdefTy ← inferType hdefVal
@@ -301,7 +321,7 @@ def simpAndIntroDef (name : String) (hdefVal : Expr) : TacticM FVarId  := do
     let hdefVal ← simpResult.mkCast hdefVal
     let hdefTy ← inferType hdefVal
 
-    let goal ← goal.define name hdefTy hdefVal
+    let goal ← goal.assert name hdefTy hdefVal
     let (fvar, goal) ← goal.intro1P
     replaceMainGoal [goal]
     return fvar
@@ -408,7 +428,7 @@ partial def MemPairwiseSeparateProof.ofExpr? (e : Expr) : Option MemPairwiseSepa
 /-- Match an expression `h` to see if it's a useful hypothesis. -/
 def hypothesisOfExpr (h : Expr) (hyps : Array Hypothesis) : MetaM (Array Hypothesis) := do
   let ht ← inferType h
-  trace[simp_mem.info] "{processingEmoji} Processing '{h}' : '{toString ht}'"
+  trace[simp_mem.info] "{processingEmoji} Processing '{h}' : '{ht}'"
   if let .some sep := MemSeparateProp.ofExpr? ht then
     let proof : MemSeparateProof sep := ⟨h⟩
     let hyps := hyps.push (.separate proof)
@@ -749,4 +769,32 @@ def proveWithOmega?  {α : Type} [ToMessageData α] [OmegaReducible α] (e : α)
     return none
   end ReductionToOmega
 
+/--
+simplify the goal state, closing legality, subset, and separation goals,
+and simplifying all other expressions. return `true` if goal has been closed, and `false` otherwise.
+-/
+partial def closeMemSideCondition (g : MVarId)
+    (bvToNatSimpCtx : Simp.Context) (bvToNatSimprocs : Array Simp.Simprocs)
+    (hyps : Array Memory.Hypothesis) : TacticM Bool := do
+  g.withContext do
+    trace[simp_mem.info] "{processingEmoji} Matching on ⊢ {← g.getType}"
+    let gt ← g.getType
+    if let .some e := MemLegalProp.ofExpr? gt then
+      TacticM.withTraceNode' m!"Matched on ⊢ {e}. Proving..." do
+        if let .some proof ← proveWithOmega? e bvToNatSimpCtx bvToNatSimprocs hyps then
+          g.assign proof.h
+    if let .some e := MemSubsetProp.ofExpr? gt then
+      TacticM.withTraceNode' m!"Matched on ⊢ {e}. Proving..." do
+        if let .some proof ← proveWithOmega? e bvToNatSimpCtx bvToNatSimprocs hyps then
+          g.assign proof.h
+    if let .some e := MemSeparateProp.ofExpr? gt then
+      TacticM.withTraceNode' m!"Matched on ⊢ {e}. Proving..." do
+        if let .some proof ← proveWithOmega? e bvToNatSimpCtx bvToNatSimprocs hyps then
+          g.assign proof.h
+  return ← g.isAssigned
+
+
+
+
+
 end Tactic.Memory
diff --git a/Arm/Memory/MemOmega.lean b/Arm/Memory/MemOmega.lean
new file mode 100644
index 00000000..23c9c458
--- /dev/null
+++ b/Arm/Memory/MemOmega.lean
@@ -0,0 +1,134 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author(s): Siddharth Bhat
+
+In this file, we define proof automation for separation conditions of memory.
+
+References:
+- https://github.com/leanprover/lean4/blob/240ebff549a2cf557f9abe9568f5de885f13e50d/src/Lean/Elab/Tactic/Omega/OmegaM.lean
+- https://github.com/leanprover/lean4/blob/240ebff549a2cf557f9abe9568f5de885f13e50d/src/Lean/Elab/Tactic/Omega/Frontend.lean
+-/
+import Arm
+import Arm.Memory.MemoryProofs
+import Arm.BitVec
+import Arm.Memory.Attr
+import Arm.Memory.AddressNormalization
+import Lean
+import Lean.Meta.Tactic.Rewrite
+import Lean.Meta.Tactic.Rewrites
+import Lean.Elab.Tactic.Conv
+import Lean.Elab.Tactic.Conv.Basic
+import Tactics.Simp
+import Tactics.BvOmegaBench
+import Arm.Memory.Common
+
+open Lean Meta Elab Tactic Memory
+
+namespace MemOmega
+
+structure Config where
+  /--
+    If true, then MemOmega will explode uses of pairwiseSeparate [mem₁, ... memₙ]
+    into O(n^2) separation conditions.
+  -/
+  explodePairwiseSeparate : Bool := false
+
+/-- Edit the config for mem_omega! -/
+def Config.mkBang (c : Config) : Config :=
+  { c with explodePairwiseSeparate := true }
+
+/-- Context for the `SimpMemM` monad, containing the user configurable options. -/
+structure Context where
+  /-- User configurable options for `simp_mem`. -/
+  cfg : Config
+  /-- Cache of `bv_toNat` simp context. -/
+  bvToNatSimpCtx : Simp.Context
+  /-- Cache of `bv_toNat` simprocs. -/
+  bvToNatSimprocs : Array Simp.Simprocs
+
+
+namespace Context
+
+def init (cfg : Config) : MetaM Context := do
+  let (bvToNatSimpCtx, bvToNatSimprocs) ←
+    LNSymSimpContext
+      (config := {failIfUnchanged := false})
+      -- Also use `mem_{legal', subset', separate'}.iff_omega to unfold definitions that
+      -- occur inside compound expressions, such as (mem_subset' .. ∨ mem_subset' ..)
+      -- (thms := #[``mem_legal'.iff_omega, ``mem_subset'.iff_omega, ``mem_separate'.iff_omega])
+      (simp_attrs := #[`bv_toNat])
+      (useDefaultSimprocs := false)
+  return {cfg, bvToNatSimpCtx, bvToNatSimprocs}
+end Context
+
+abbrev MemOmegaM := (ReaderT Context TacticM)
+
+namespace MemOmegaM
+
+  def run (ctx : Context) (x : MemOmegaM α) : TacticM α := ReaderT.run x ctx
+
+end MemOmegaM
+
+def memOmegaTac : MemOmegaM Unit := do
+  let g ← getMainGoal
+  g.withContext do
+    /- We need to explode all pairwise separate hyps -/
+    let rawHyps ← getLocalHyps
+    let mut hyps := #[]
+    -- extract out structed values for all hyps.
+    for h in rawHyps do
+      hyps ← hypothesisOfExpr h hyps
+
+    -- only enable pairwise constraints if it is enabled.
+    let isPairwiseEnabled := (← readThe Context).cfg.explodePairwiseSeparate
+    hyps := hyps.filter (!·.isPairwiseSeparate || isPairwiseEnabled)
+
+    -- used specialized procedure that doesn't unfold everything for the easy case.
+    if ← closeMemSideCondition (← getMainGoal) (← readThe Context).bvToNatSimpCtx (← readThe Context).bvToNatSimprocs hyps then
+      return ()
+    else
+      -- in the bad case, just rip through everything.
+      -- let _ ← Hypothesis.addOmegaFactsOfHyps (hyps.toList.filter (fun h => h.isPairwiseSeparate)) #[]
+      let _ ← Hypothesis.addOmegaFactsOfHyps hyps.toList #[]
+
+      TacticM.withTraceNode' m!"Reducion to omega" do
+        try
+          TacticM.traceLargeMsg m!"goal (Note: can be large)"  m!"{← getMainGoal}"
+          omega (← readThe Context).bvToNatSimpCtx (← readThe Context).bvToNatSimprocs
+          trace[simp_mem.info] "{checkEmoji} `omega` succeeded."
+        catch e =>
+          trace[simp_mem.info]  "{crossEmoji} `omega` failed with error:\n{e.toMessageData}"
+
+
+/--
+Allow elaboration of `MemOmegaConfig` arguments to tactics.
+-/
+declare_config_elab elabMemOmegaConfig MemOmega.Config
+
+/--
+Implement the `mem_omega` tactic, which unfolds information about memory
+in terms of
+-/
+syntax (name := mem_omega) "mem_omega" (Lean.Parser.Tactic.config)? : tactic
+
+/--
+Implement the `mem_omega` tactic frontend.
+-/
+syntax (name := mem_omega_bang) "mem_omega!" (Lean.Parser.Tactic.config)? : tactic
+
+@[tactic mem_omega]
+def evalMemOmega : Tactic := fun
+  | `(tactic| mem_omega $[$cfg]?) => do
+    let cfg ← elabMemOmegaConfig (mkOptionalNode cfg)
+    memOmegaTac.run (← Context.init cfg)
+  | _ => throwUnsupportedSyntax
+
+@[tactic mem_omega_bang]
+def evalMemOmegaBang : Tactic := fun
+  | `(tactic| mem_omega! $[$cfg]?) => do
+    let cfg ← elabMemOmegaConfig (mkOptionalNode cfg)
+    memOmegaTac.run (← Context.init cfg.mkBang)
+  | _ => throwUnsupportedSyntax
+
+end MemOmega
diff --git a/Arm/Memory/Separate.lean b/Arm/Memory/Separate.lean
index 99c6bdcc..d42338f1 100644
--- a/Arm/Memory/Separate.lean
+++ b/Arm/Memory/Separate.lean
@@ -230,12 +230,12 @@ theorem mem_legal'.omega_def (h : mem_legal' a n) : a.toNat + n ≤ 2^64 := h
 
 /-- The linear constraint is equivalent to `mem_legal'`. -/
 theorem mem_legal'.iff_omega (a : BitVec 64) (n : Nat) :
-    (a.toNat + n ≤ 2^64) ↔ mem_legal' a n := by
+    mem_legal' a n ↔ (a.toNat + n ≤ 2^64) := by
   constructor
-  · intros h
-    apply mem_legal'.of_omega h
   · intros h
     apply h.omega_def
+  · intros h
+    apply mem_legal'.of_omega h
 
 instance : Decidable (mem_legal' a n) :=
   if h : a.toNat + n ≤ 2^64 then
@@ -341,14 +341,15 @@ theorem mem_separate'.of_omega
 
 /-- The linear constraint is equivalent to `mem_separate'`. -/
 theorem mem_separate'.iff_omega (a : BitVec 64) (an : Nat) (b : BitVec 64) (bn : Nat) :
+    mem_separate' a an b bn ↔
     (a.toNat + an ≤ 2^64 ∧
     b.toNat + bn ≤ 2^64 ∧
-    (a.toNat + an ≤ b.toNat ∨ a.toNat ≥ b.toNat + bn)) ↔ mem_separate' a an b bn := by
+    (a.toNat + an ≤ b.toNat ∨ a.toNat ≥ b.toNat + bn)) := by
   constructor
-  · intros h
-    apply mem_separate'.of_omega h
   · intros h
     apply h.omega_def
+  · intros h
+    apply mem_separate'.of_omega h
 
 instance : Decidable (mem_separate' a an b bn) :=
   if h : (a.toNat + an ≤ 2^64 ∧ b.toNat + bn ≤ 2^64 ∧ (a.toNat + an ≤ b.toNat ∨ a.toNat ≥ b.toNat + bn)) then
@@ -424,15 +425,16 @@ constructor
 
 /-- The linear constraint is equivalent to `mem_subset'`. -/
 theorem mem_subset'.iff_omega (a : BitVec 64) (an : Nat) (b : BitVec 64) (bn : Nat) :
+    mem_subset' a an b bn  ↔
     (a.toNat + an ≤ 2^64 ∧
     b.toNat + bn ≤ 2^64 ∧
     b.toNat ≤ a.toNat ∧
-    a.toNat + an ≤ b.toNat + bn) ↔ mem_subset' a an b bn := by
+    a.toNat + an ≤ b.toNat + bn) := by
   constructor
-  · intros h
-    apply mem_subset'.of_omega h
   · intros h
     apply h.omega_def
+  · intros h
+    apply mem_subset'.of_omega h
 
 instance : Decidable (mem_subset' a an b bn) :=
   if h : (a.toNat + an ≤ 2^64 ∧ b.toNat + bn ≤ 2^64 ∧ b.toNat ≤ a.toNat ∧ a.toNat + an ≤ b.toNat + bn) then
@@ -681,4 +683,21 @@ def Memory.Region.separate'_of_pairwiseSeprate_of_mem_of_mem
         · simp only [List.get?_eq_getElem?, ha]
         · simp only [List.get?_eq_getElem?, hb]
 
+
+/--
+Convenient API to extract out a separate proof from a Memory.Region.pairwiseSeparate.
+Proof obligations are given by `decide` to allow the API to be used as follows:
+
+let h := mem.pairwiseSeparate [(a, na), (b, nb), (c, nc)]
+let h01 := h.get 0 1
+-/
+def Memory.Region.pairwiseSeparate.get
+    (h : Memory.Region.pairwiseSeparate mems)
+    (i j : Nat)
+    (hi : i < mems.length := by simp)
+    (hj : j < mems.length := by simp)
+    (hij : i ≠ j := by omega) :
+    mem_separate' mems[i].fst mems[i].snd mems[j].fst mems[j].snd := by
+  apply Memory.Region.separate'_of_pairwiseSeprate_of_mem_of_mem h i j hij <;> simp
+
 end NewDefinitions
diff --git a/Arm/Memory/SeparateAutomation.lean b/Arm/Memory/SeparateAutomation.lean
index 5517064b..786b96e5 100644
--- a/Arm/Memory/SeparateAutomation.lean
+++ b/Arm/Memory/SeparateAutomation.lean
@@ -23,6 +23,7 @@ import Lean.Elab.Tactic.Conv.Basic
 import Tactics.Simp
 import Tactics.BvOmegaBench
 import Arm.Memory.Common
+import Arm.Memory.MemOmega
 
 open Lean Meta Elab Tactic Memory
 
@@ -107,18 +108,6 @@ structure SimpMemConfig where
   rewriteFuel : Nat := 1000
   /-- whether an error should be thrown if the tactic makes no progress. -/
   failIfUnchanged : Bool := true
-  /-- whether `simp_mem` should always try to use `omega` to close the goal,
-    even if goal state is not recognized as one of the blessed states.
-    This is useful when one is trying to establish some numerical invariant
-    about addresses based on knowledge of memory.
-    e.g.
-    ```
-    h : mem_separate' a 10 b 10
-    hab : a < b
-    ⊢ a + 5 < b
-    ```
-  -/
-  useOmegaToClose : Bool := false
 
 /-- Context for the `SimpMemM` monad, containing the user configurable options. -/
 structure Context where
@@ -288,48 +277,6 @@ partial def SimpMemM.simplifyExpr (e : Expr) (hyps : Array Memory.Hypothesis) :
       | _ => return false
 
 
-/--
-simplify the goal state, closing legality, subset, and separation goals,
-and simplifying all other expressions. return `true` if goal has been closed, and `false` otherwise.
--/
-partial def SimpMemM.closeGoal (g : MVarId) (hyps : Array Memory.Hypothesis) : SimpMemM Bool := do
-  SimpMemM.withContext g do
-    trace[simp_mem.info] "{processingEmoji} Matching on ⊢ {← g.getType}"
-    let gt ← g.getType
-    if let .some e := MemLegalProp.ofExpr? gt then
-      withTraceNode m!"Matched on ⊢ {e}. Proving..." do
-        if let .some proof ← proveWithOmega? e (← getBvToNatSimpCtx) (← getBvToNatSimprocs) hyps then
-          g.assign proof.h
-    if let .some e := MemSubsetProp.ofExpr? gt then
-      withTraceNode m!"Matched on ⊢ {e}. Proving..." do
-        if let .some proof ← proveWithOmega? e (← getBvToNatSimpCtx) (← getBvToNatSimprocs) hyps then
-          g.assign proof.h
-    if let .some e := MemSeparateProp.ofExpr? gt then
-      withTraceNode m!"Matched on ⊢ {e}. Proving..." do
-        if let .some proof ← proveWithOmega? e (← getBvToNatSimpCtx) (← getBvToNatSimprocs) hyps then
-          g.assign proof.h
-
-    if (← getConfig).useOmegaToClose then
-      withTraceNode m!"Unknown memory expression ⊢ {gt}. Trying reduction to omega (`config.useOmegaToClose = true`):" do
-        let oldGoals := (← getGoals)
-        try
-          let gproof ← mkFreshExprMVar (type? := gt)
-          setGoals (gproof.mvarId! :: (← getGoals))
-          SimpMemM.withMainContext do
-          let _ ← Hypothesis.addOmegaFactsOfHyps hyps.toList #[]
-          trace[simp_mem.info] m!"Executing `omega` to close {gt}"
-          SimpMemM.withTraceNode m!"goal (Note: can be large)" do
-            trace[simp_mem.info] "{← getMainGoal}"
-          omega (← getBvToNatSimpCtx) (← getBvToNatSimprocs)
-          trace[simp_mem.info] "{checkEmoji} `omega` succeeded."
-          g.assign gproof
-        catch e =>
-          trace[simp_mem.info]  "{crossEmoji} `omega` failed with error:\n{e.toMessageData}"
-          setGoals oldGoals
-  return ← g.isAssigned
-
-
-
 /--
 simplify the goal state, closing legality, subset, and separation goals,
 and simplifying all other expressions. Returns `true` if an improvement has been made
@@ -361,10 +308,6 @@ partial def SimpMemM.simplifyLoop : SimpMemM Unit := do
       for (i, h) in foundHyps.toList.enum do
         trace[simp_mem.info] m!"{i+1}) {h}"
 
-    if ← SimpMemM.closeGoal g foundHyps then
-      trace[simp_mem.info] "{checkEmoji} goal closed."
-      return ()
-
     -- goal was not closed, try and improve.
     let mut changedInAnyIter? := false
     while true do
diff --git a/Proofs/AES-GCM/GCMGmultV8Sym.lean b/Proofs/AES-GCM/GCMGmultV8Sym.lean
index c759ef80..dcc60c7b 100644
--- a/Proofs/AES-GCM/GCMGmultV8Sym.lean
+++ b/Proofs/AES-GCM/GCMGmultV8Sym.lean
@@ -119,11 +119,11 @@ theorem gcm_gmult_v8_program_run_27 (s0 sf : ArmState)
     simp_mem; rfl
     -/
     rw [Memory.read_bytes_write_bytes_eq_read_bytes_of_mem_separate']
-    simp_mem
+    mem_omega!
   · simp only [List.mem_cons, List.mem_singleton, not_or, and_imp]
     sym_aggregate
   · intro n addr h_separate
-    simp_mem (config := { useOmegaToClose := false })
+    simp_mem
     -- Aggregate the memory (non)effects.
     simp only [*]
   · clear_named [h_s, stepi_]
@@ -135,7 +135,14 @@ theorem gcm_gmult_v8_program_run_27 (s0 sf : ArmState)
       rw [@Memory.read_bytes_eq_extractLsBytes_sub_of_mem_subset'
            32 (r (StateField.GPR 1#5) s0) HTable (r (StateField.GPR 1#5) s0) 16 _ h_HTable.symm]
       · simp only [Nat.reduceMul, BitVec.extractLsBytes, Nat.sub_self, Nat.zero_mul]
-      · simp_mem
+      · mem_omega!
+        -- have := h_mem_sep.get 0 1
+        -- simp at this
+        -- rw [mem_separate'.iff_omega] at this
+        -- mem_omega!
+        -- mem_omega!
+        -- simp_all
+
     have h_HTable_high :
       (Memory.read_bytes 16 (r (StateField.GPR 1#5) s0 + 16#64) s0.mem) = HTable.extractLsb' 128 128 := by
       -- (FIXME @bollu) use `simp_mem` instead of the rw below.
diff --git a/Proofs/Experiments/Max/MaxTandem.lean b/Proofs/Experiments/Max/MaxTandem.lean
index e75925a0..3a66591f 100644
--- a/Proofs/Experiments/Max/MaxTandem.lean
+++ b/Proofs/Experiments/Max/MaxTandem.lean
@@ -626,7 +626,7 @@ theorem partial_correctness :
       -- 2/15
       name h_s1_run : s2 := run 1 s1
       obtain ⟨h_s2_cut, h_s2_pc, h_s2_err, h_s2_program, h_s2_read_sp_8, h_s2_read_sp_12, h_s2_x0, h_s2_x1, h_s2_sp, h_s2_sp_aligned⟩ :=
-        program.stepi_0x898_cut s1 s2 h_s1_program h_s1_pc h_s1_err h_s1_sp_aligned (by simp_mem) h_s1_run.symm
+        program.stepi_0x898_cut s1 s2 h_s1_program h_s1_pc h_s1_err h_s1_sp_aligned (by mem_omega) h_s1_run.symm
       rw [Correctness.snd_cassert_of_not_cut h_s2_cut]; -- try rw [Correctness.snd_cassert_of_cut h_cut];
       simp [show Sys.next s2 = run 1 s2 by rfl]
       replace h_s2_sp : s2.sp = (s0.sp - 32#64) := by simp_all
@@ -637,7 +637,7 @@ theorem partial_correctness :
 
       -- 3/15
       name h_run : s3 := run 1 s2
-      obtain h := program.stepi_0x89c_cut s2 s3 h_s2_program h_s2_pc h_s2_err h_s2_sp_aligned (by simp_mem) h_run.symm
+      obtain h := program.stepi_0x89c_cut s2 s3 h_s2_program h_s2_pc h_s2_err h_s2_sp_aligned (by mem_omega) h_run.symm
       obtain ⟨h_s3_cut, h_s3_read_sp_8, h_s3_read_sp_12, h_s3_x0, h_s3_x1, h_s3_sp, h_s3_pc, h_s3_err, h_s3_program, h_s3_sp_aligned⟩ := h
       rw [Correctness.snd_cassert_of_not_cut h_s3_cut]; -- try rw [Correctness.snd_cassert_of_cut h_cut];
       simp [show Sys.next s3 = run 1 s3 by rfl]
diff --git a/Proofs/Experiments/Memcpy/MemCpyVCG.lean b/Proofs/Experiments/Memcpy/MemCpyVCG.lean
index 4b4a7ce1..556a7f40 100644
--- a/Proofs/Experiments/Memcpy/MemCpyVCG.lean
+++ b/Proofs/Experiments/Memcpy/MemCpyVCG.lean
@@ -468,11 +468,11 @@ theorem Memcpy.extracted_2 (s0 si : ArmState)
   have h_upper_bound := hsep.hb.omega_def
   have h_upper_bound₂ := h_pre_1.hb.omega_def
   have h_upper_bound₃ := hsep.ha.omega_def
-  have h_width_lt : (0x10#64).toNat * (s0.x0 - (si.x0 - 0x1#64)).toNat < 2 ^ 64 := by simp_mem (config := {useOmegaToClose := true})
+  have h_width_lt : (0x10#64).toNat * (s0.x0 - (si.x0 - 0x1#64)).toNat < 2 ^ 64 := by mem_omega
   rw [Memory.read_bytes_write_bytes_eq_read_bytes_of_mem_separate']
   · rw [h_assert_6]
-    skip_proof simp_mem
-  · -- @bollu: TODO: figure out why this is so slow!
+    skip_proof mem_omega
+  · -- @bollu: TODO: figure out why this is so slow!/
     apply mem_separate'.symm
     apply mem_separate'.of_subset'_of_subset' hsep
     · apply mem_subset'.of_omega
@@ -516,9 +516,9 @@ theorem Memcpy.extracted_0 (s0 si : ArmState)
   apply And.intro
   · intros i hi
     have h_subset_2 : mem_subset' s0.x2 (0x10#64 * (s0.x0 - si.x0)).toNat s0.x2 (s0.x0.toNat * 16) := by
-      skip_proof simp_mem
+      skip_proof mem_omega
     have h_subset_1 : mem_subset' (s0.x1 + 0x10#64 * (s0.x0 - si.x0)) 16 s0.x1 (s0.x0.toNat * 16) := by
-      skip_proof simp_mem
+      skip_proof mem_omega
     have icases : i = s0.x0 - si.x0 ∨ i < s0.x0 - si.x0 := by skip_proof bv_omega_bench
     have s2_sum_inbounds := h_pre_1.hb.omega_def
     have i_sub_x0_mul_16 : 16 * i.toNat < 16 * s0.x0.toNat := by skip_proof bv_omega_bench
@@ -529,13 +529,13 @@ theorem Memcpy.extracted_0 (s0 si : ArmState)
       · simp only [Nat.reduceMul, BitVec.toNat_add, BitVec.toNat_mul, BitVec.toNat_ofNat,
         Nat.reducePow, Nat.reduceMod, BitVec.toNat_sub, Nat.add_mod_mod, Nat.sub_self,
         BitVec.extractLsBytes_eq_self, BitVec.cast_eq]
-        rw [h_assert_6 _ _ (by simp_mem)]
-      · skip_proof simp_mem
+        rw [h_assert_6 _ _ (by mem_omega)]
+      · skip_proof mem_omega
     · rw [Memory.read_bytes_write_bytes_eq_read_bytes_of_mem_separate']
       · apply h_assert_5 _ hi
       · constructor
-        · skip_proof simp_mem
-        · skip_proof simp_mem
+        · skip_proof mem_omega
+        · skip_proof mem_omega
         · left
           -- @bollu: TODO, see if `simp_mem` can figure this out given less aggressive
           -- proof states.
@@ -670,7 +670,7 @@ theorem partial_correctness :
             simp only [memory_rules] at h_si_read_sep
             rw [h_si_read_sep]
             rw [h_si_x0_eq_zero]
-            skip_proof simp_mem -- nice!
+            skip_proof mem_omega -- nice!
           · simp only [step.h_err, step.h_program, step.h_sp_aligned, and_self]
       · have step_8f4_8e4 :=
           program.step_8f4_8e4_of_wellformed_of_z_eq_0 si s1 si_well_formed
diff --git a/Proofs/Experiments/MemoryAliasing.lean b/Proofs/Experiments/MemoryAliasing.lean
index b7ac1b9c..3d665292 100644
--- a/Proofs/Experiments/MemoryAliasing.lean
+++ b/Proofs/Experiments/MemoryAliasing.lean
@@ -17,7 +17,7 @@ import Arm.Memory.SeparateAutomation
 namespace MemLegal
 /-- Show reflexivity of legality. -/
 theorem legal_1 (l : mem_legal' a 16) : mem_legal' a 16 := by
-  simp_mem
+  mem_omega
 
 /-- info: 'MemLegal.legal_1' depends on axioms: [propext, Quot.sound] -/
 #guard_msgs in #print axioms legal_1
@@ -27,28 +27,28 @@ end MemLegal
 namespace MemSubset
 /-- Reflexivity. -/
 theorem subset_1 (l : mem_subset' a 16 b 16) : mem_subset' a 16 b 16 := by
-  simp_mem
+  mem_omega
 
 /-- info: 'MemSubset.subset_1' depends on axioms: [propext, Classical.choice, Quot.sound] -/
 #guard_msgs in #print axioms subset_1
 
 /-- Show that smaller subsets are also subsets. -/
 theorem subset_2 (l : mem_subset' a 16 b 16) : mem_subset' a 10 b 16 := by
-  simp_mem
+  mem_omega
 
 /-- info: 'MemSubset.subset_2' depends on axioms: [propext, Classical.choice, Quot.sound] -/
 #guard_msgs in #print axioms subset_2
 
 /-- Show that smaller subsets are also subsets, even when moving base pointer. -/
 theorem subset_3 (l : mem_subset' a 16 b 16) : mem_subset' (a+6) 10 b 16 := by
-  simp_mem
+  mem_omega
 
 /-- info: 'MemSubset.subset_3' depends on axioms: [propext, Classical.choice, Quot.sound] -/
 #guard_msgs in #print axioms subset_3
 
 /-- Show that we can perform address arithmetic based on subset constraints. -/
 theorem subset_4 (l : mem_subset' a 16 b 16) : a = b := by
-  simp_mem (config := {useOmegaToClose := true})
+  mem_omega
 
 /-- Show that we can perform address arithmetic based on subset constraints.
 Only two configurations possible:
@@ -60,7 +60,7 @@ a0 a1 a2 ..
 b0 b1 b2 b3
 -/
 theorem subset_5 (l : mem_subset' a 3 b 4) : a ≤ b + 1 := by
-  simp_mem (config := {useOmegaToClose := true})
+  mem_omega
 
 end MemSubset
 
@@ -68,7 +68,7 @@ namespace MemSeparate
 
 /-- Reflexivity. -/
 theorem separate_1 (l : mem_separate' a 16 b 16) : mem_separate' a 16 b 16 := by
-  simp_mem
+  mem_omega
 
 /-- info: 'MemSeparate.separate_1' depends on axioms: [propext, Classical.choice, Quot.sound] -/
 #guard_msgs in #print axioms separate_1
@@ -76,14 +76,14 @@ theorem separate_1 (l : mem_separate' a 16 b 16) : mem_separate' a 16 b 16 := by
 
 /-- Symmetry. -/
 theorem separate_2 (l : mem_separate' a 16 b 16) : mem_separate' b 16 a 16 := by
-  simp_mem
+  mem_omega
 
 /-- info: 'MemSeparate.separate_2' depends on axioms: [propext, Classical.choice, Quot.sound] -/
 #guard_msgs in #print axioms separate_2
 
 /-- Smaller subsets. -/
 theorem separate_3 (l : mem_separate' a 16 b 16) : mem_separate' b 10 a 10 := by
-  simp_mem
+  mem_omega
 
 /-- info: 'MemSeparate.separate_3' depends on axioms: [propext, Classical.choice, Quot.sound] -/
 #guard_msgs in #print axioms separate_3
@@ -91,7 +91,7 @@ theorem separate_3 (l : mem_separate' a 16 b 16) : mem_separate' b 10 a 10 := by
 /-- sliding subset to the right. -/
 theorem separate_4 (l : mem_separate' a 16 b 16) (hab : a < b) :
     mem_separate' a 17 (b+1) 15 := by
-  simp_mem
+  mem_omega
 
 /-- info: 'MemSeparate.separate_4' depends on axioms: [propext, Classical.choice, Quot.sound] -/
 #guard_msgs in #print axioms separate_4
@@ -100,7 +100,7 @@ theorem separate_4 (l : mem_separate' a 16 b 16) (hab : a < b) :
 theorem separate_5 {n : Nat} (hn : n ≠ 0)
     (l : mem_separate' a (n <<< 4) b (n <<< 4))  :
     mem_separate' a 16 b 16 := by
-  simp_mem
+  mem_omega
 
 /-- info: 'MemSeparate.separate_5' depends on axioms: [propext, Classical.choice, Quot.sound] -/
 #guard_msgs in #print axioms separate_5
@@ -109,7 +109,7 @@ theorem separate_5 {n : Nat} (hn : n ≠ 0)
 theorem separate_6 {n : Nat} (hn : n ≠ 0)
     (l : mem_separate' a (n <<< 4) b (n <<< 4))  :
     mem_separate' a (n <<< 3 + 8) b (n <<< 4) := by
-  simp_mem
+  mem_omega
 
 /-- info: 'MemSeparate.separate_6' depends on axioms: [propext, Classical.choice, Quot.sound] -/
 #guard_msgs in #print axioms separate_6
@@ -136,7 +136,7 @@ us to exploit memory separateness properties.
 -/
 theorem mem_separate_9  (h : mem_separate' a 100 b 100)
   (hab : a < b) : a + 50 ≤ b := by
-  simp_mem (config := {useOmegaToClose := true})
+  mem_omega
 
 end MemSeparate
 
@@ -374,7 +374,7 @@ proving generic properties about our definitions of `mem_legal'`,
 -/
 
 /-! ### mem_subset is a partial order. -/
-theorem mem_subset_refl (h : mem_legal' a an) : mem_subset' a an a an := by simp_mem
+theorem mem_subset_refl (h : mem_legal' a an) : mem_subset' a an a an := by mem_omega
 /-
 TODO(@bollu): In such a scenario, we should call `omega` directly on the goal,
 and see if it can solve it.
@@ -383,35 +383,41 @@ theorem mem_subset_asymm (h : mem_subset' a an b bn) (h' : mem_subset' b bn a an
   simp_mem
 -/
 theorem mem_subset_trans (h : mem_subset' a an b bn) (h' : mem_subset' b bn c cn) :
-  mem_subset' a an c cn := by simp_mem
+  mem_subset' a an c cn := by mem_omega
 
 /-! ### mem_separate relationship to arithmetic -/
 
-theorem mem_separate_comm (h : mem_separate' a an b bn) : mem_separate' b bn a an := by simp_mem
+theorem mem_separate_comm (h : mem_separate' a an b bn) : mem_separate' b bn a an := by mem_omega
 /-- if `[a..an)⟂[b..bn)`, then `[a+δ..an-δ)⟂[b..bn)`-/
 theorem mem_separate_of_lt_of_lt_sub (h : mem_separate' a an b bn) (hab : a < b)
-  (hδ : δ < b - a): mem_separate' (a + δ) (an - δ.toNat) b bn := by simp_mem
+  (hδ : δ < b - a): mem_separate' (a + δ) (an - δ.toNat) b bn := by mem_omega
 /-- If `[a..an)⟂[b..bn)`, and `a ≤ b`, then `[a'..an+(a-a'))⟂[b..bn)`.
 This lets us increase the size of the left memory region.
 -/
 theorem mem_separate_move_of_lt_of_le  (h : mem_separate' a an b bn)
   (hab : a < b)
-  (hlegal : a' ≤ a) : mem_separate' a' (an + (a - a').toNat) b bn := by simp_mem
+  (hlegal : a' ≤ a) : mem_separate' a' (an + (a - a').toNat) b bn := by mem_omega
 
 end MathProperties
 
 
-
 section PairwiseSeparate
   /- Check that a direct implication of the pairwise separation is proven. -/
   theorem pairwise_direct (h : Memory.Region.pairwiseSeparate [⟨a, 100⟩, ⟨b, 200⟩, ⟨c, 300⟩, ⟨d, 400⟩]) :
     mem_separate' a 100 b 200 := by
-    simp_mem
+    mem_omega (config := {explodePairwiseSeparate := true})
+
+  /- Check that a direct implication of the pairwise separation is proven. -/
+  theorem pairwise_direct' (h : Memory.Region.pairwiseSeparate [⟨a, 100⟩, ⟨b, 200⟩, ⟨c, 300⟩, ⟨d, 400⟩]) :
+    mem_separate' a 100 b 200 := by
+    mem_omega! -- use the notation to exploit every hypothesis.
 
   /- Check that a direct implication of the pairwise separation is proven. -/
   theorem pairwise_subset (h : Memory.Region.pairwiseSeparate [⟨a, 100⟩, ⟨b, 200⟩, ⟨c, 300⟩, ⟨d, 400⟩]) :
     mem_separate' a 80 b 100 := by
-    simp_mem
+    have := h.get 0 1
+    simp at this
+    mem_omega -- intro useful hypothesis and use it.
 
 end PairwiseSeparate
 
@@ -425,7 +431,6 @@ error: unsolved goals
 ---
 info: [simp_mem.info] Searching for Hypotheses
 [simp_mem.info] Summary: Found 0 hypotheses
-[simp_mem.info] ⚙️ Matching on ⊢ False
 [simp_mem.info] Performing Rewrite At Main Goal
   [simp_mem.info] Simplifying goal.
 [simp_mem.info] ❌️ No progress made in this iteration. halting.
@@ -443,7 +448,6 @@ error: ❌️ simp_mem failed to make any progress.
 ---
 info: [simp_mem.info] Searching for Hypotheses
 [simp_mem.info] Summary: Found 0 hypotheses
-[simp_mem.info] ⚙️ Matching on ⊢ False
 [simp_mem.info] Performing Rewrite At Main Goal
   [simp_mem.info] Simplifying goal.
 [simp_mem.info] ❌️ No progress made in this iteration. halting.
diff --git a/Proofs/Popcount32.lean b/Proofs/Popcount32.lean
index cb71dbf4..10ef79a4 100644
--- a/Proofs/Popcount32.lean
+++ b/Proofs/Popcount32.lean
@@ -103,8 +103,7 @@ theorem popcount32_sym_meets_spec (s0 sf : ArmState)
   · -- Memory Frame Condition
     intro n addr h_separate
     simp only [memory_rules] at *
-    repeat (simp_mem (config := { useOmegaToClose := false }); sym_aggregate)
-
+    repeat (simp_mem; sym_aggregate)
   done
 
 /--
diff --git a/Proofs/SHA512/SHA512Prelude.lean b/Proofs/SHA512/SHA512Prelude.lean
index 9013de0c..86326ba8 100644
--- a/Proofs/SHA512/SHA512Prelude.lean
+++ b/Proofs/SHA512/SHA512Prelude.lean
@@ -182,7 +182,7 @@ theorem sha512_block_armv8_prelude (s0 sf : ArmState)
   · constructor
     · -- (TODO @bollu) Think about whether `simp_mem` should be powerful enough to solve this goal.
       -- Also, `mem_omega` name suggestion from Alex for the already souped up `simp_mem`.
-      simp_mem (config := { useOmegaToClose := false } )
+      simp_mem
       simp only [h_s0_ctx_base, Nat.sub_self, minimal_theory, bitvec_rules]
     · constructor
       · -- (FIXME @bollu) simp_mem doesn't make progress here. :-(