diff --git a/lean/Spa/Language/Graphs.lean b/lean/Spa/Language/Graphs.lean
index 6d285a1..d3a9e03 100644
--- a/lean/Spa/Language/Graphs.lean
+++ b/lean/Spa/Language/Graphs.lean
@@ -229,55 +229,47 @@ because of the offset-based embedding, we can determine whether a node
 came from a particular subgraph simply by examining its offset and sub-graph
 size. This is captured by `Embed.mem_range_iff`. -/
 
-/-- Translate an index of `g` into `h` by a constant offset. -/
-private def shift {g h : GGraph α} (off : ℕ) (hle : g.size + off ≤ h.size) (i : g.Index) :
-    h.Index := ⟨off + i.val, by omega⟩
-
-@[simp] lemma shift_val {g h : GGraph α} {off : ℕ} (hle : g.size + off ≤ h.size)
-    (i : g.Index) : (shift (h := h) off hle i).val = off + i.val := rfl
-
 /-- A special-case embedding of `g` into `h` in which all edges and nodes
     of `g` are present in `h` at a given offset `off`. -/
 structure Embed (g h : GGraph α) where
+  f : g.Index → h.Index
   off : ℕ
-  size_le : g.size + off ≤ h.size
-  nodes_eq : ∀ i, h.nodes (shift off size_le i) = g.nodes i
-  edges_mem : ∀ {e : g.Edge}, e ∈ g.edges →
-    (shift off size_le e.1, shift off size_le e.2) ∈ h.edges
+  f_val : ∀ i, (f i).val = off + i.val
+  nodes_eq : ∀ i, h.nodes (f i) = g.nodes i
+  edges_mem : ∀ {e : g.Edge}, e ∈ g.edges → (f e.1, f e.2) ∈ h.edges
 
-/-- The index translation of an embedding. -/
-abbrev Embed.f {g h : GGraph α} (e : Embed g h) (i : g.Index) : h.Index :=
-  shift e.off e.size_le i
-
-lemma Embed.f_inj {g h : GGraph α} (e : Embed g h) : Function.Injective e.f :=
-  fun _ _ hij => Fin.ext (by simpa using congrArg Fin.val hij)
+lemma Embed.f_inj {g h : GGraph α} (e : Embed g h) : Function.Injective e.f := by
+  intro i j hij
+  have := congrArg Fin.val hij
+  rw [e.f_val, e.f_val] at this
+  exact Fin.ext (by omega)
 
 /-- An embedding's range is the interval `[off, off + g.size)`. -/
 lemma Embed.mem_range_iff {g h : GGraph α} (e : Embed g h) (j : h.Index) :
     (∃ i, e.f i = j) ↔ e.off ≤ j.val ∧ j.val < e.off + g.size := by
   constructor
-  · rintro ⟨i, rfl⟩; have := i.isLt; simp only [Embed.f, shift_val]; omega
+  · rintro ⟨i, rfl⟩; have := i.isLt; rw [e.f_val]; omega
   · rintro ⟨hlo, hhi⟩
-    exact ⟨⟨j.val - e.off, by omega⟩, Fin.ext (by simp only [Embed.f, shift_val]; omega)⟩
+    refine ⟨⟨j.val - e.off, by omega⟩, Fin.ext ?_⟩
+    rw [e.f_val]
+    show e.off + (j.val - e.off) = j.val
+    omega
 
 /-- Build an embedding from an index map that is pointwise the shift.  The five
     inclusions below are naturally written with `Fin.castAdd`/`Fin.natAdd` — the form
     the `Fin.append` lemmas are stated in — so this lets them keep those proofs
-    verbatim while `Embed` stores only the offset.  The trailing two arguments are
-    boilerplate at every call site and default to discharging themselves. -/
+    verbatim.  The trailing argument is boilerplate at every call site and defaults
+    to discharging itself. -/
 private def Embed.ofIndexMap {g h : GGraph α} (off : ℕ) (k : g.Index → h.Index)
     (hn : ∀ i, h.nodes (k i) = g.nodes i)
     (hem : ∀ {e : g.Edge}, e ∈ g.edges → (k e.1, k e.2) ∈ h.edges)
-    (hle : g.size + off ≤ h.size := by
-      first | omega | (simp [GGraph.sequence, GGraph.overlay, GGraph.loop] <;> omega))
     (hk : ∀ i, (k i).val = off + i.val := by intro i; simp) :
     Embed g h where
+  f := k
   off := off
-  size_le := hle
-  nodes_eq i := by rw [show shift off hle i = k i from Fin.ext (by simp [hk])]; exact hn i
-  edges_mem hmem := by
-    have hs : ∀ i, shift (h := h) off hle i = k i := fun i => Fin.ext (by simp [hk])
-    rw [hs, hs]; exact hem hmem
+  f_val := hk
+  nodes_eq := hn
+  edges_mem := hem
 
 /-- Embeddings compose (offsets add). -/
 def Embed.trans {g₁ g₂ g₃ : GGraph α} (e₁ : Embed g₁ g₂) (e₂ : Embed g₂ g₃) :
@@ -285,8 +277,7 @@ def Embed.trans {g₁ g₂ g₃ : GGraph α} (e₁ : Embed g₁ g₂) (e₂ : Em
   ofIndexMap (e₂.off + e₁.off) (fun i => e₂.f (e₁.f i))
     (fun i => (e₂.nodes_eq (e₁.f i)).trans (e₁.nodes_eq i))
     (fun he => e₂.edges_mem (e₁.edges_mem he))
-    (hle := by have := e₁.size_le; have := e₂.size_le; omega)
-    (hk := fun i => by simp; omega)
+    (hk := fun i => by rw [e₂.f_val, e₁.f_val]; omega)
 
 /-- The left operand's inclusion into a sequenced graph. -/
 def Embed.sequenceLeft (g₁ g₂ : GGraph α) : Embed g₁ (g₁ ⤳ g₂) :=
@@ -322,20 +313,6 @@ def Embed.singletonIndex {a : α} {h : GGraph α} (e : Embed (singleton a) h) :
     (e : Embed (singleton a) h) : h.nodes e.singletonIndex = a :=
   e.nodes_eq ⟨0, Nat.zero_lt_one⟩
 
-/-! `shift` puts the offset on the left (`off + i.val`), matching `Fin.natAdd`, so
-every right inclusion is *definitionally* the form `Spa/Language/Properties.lean`
-states its trace indices in.  Only the left inclusions need a bridge, since their
-offset is `0` and `0 + i.val` does not reduce.
-
-Deliberately not `@[simp]`: they rewrite `Embed.f` back into `Fin.castAdd` form,
-discarding the offset that `Embed.mem_range_iff` — and the subgraph-containment
-tests built on it — reason with. -/
-
-lemma Embed.sequenceLeft_f (g₁ g₂ : GGraph α) (i : g₁.Index) :
-    (Embed.sequenceLeft g₁ g₂).f i = i.castAdd g₂.size := Fin.ext (Nat.zero_add _)
-lemma Embed.overlayLeft_f (g₁ g₂ : GGraph α) (i : g₁.Index) :
-    (Embed.overlayLeft g₁ g₂).f i = i.castAdd g₂.size := Fin.ext (Nat.zero_add _)
-
 variable (g : GGraph α)
 
 /-- All the nodes in the graph. -/
diff --git a/lean/Spa/Language/Properties.lean b/lean/Spa/Language/Properties.lean
index e1deca2..08caeb6 100644
--- a/lean/Spa/Language/Properties.lean
+++ b/lean/Spa/Language/Properties.lean
@@ -41,9 +41,8 @@ noncomputable def Trace.embed {g h : Graph} (e : GGraph.Embed g h)
     a corresponding trace exists in the combined graph. -/
 noncomputable def Trace.overlay_left {idx₁ idx₂ : g₁.Index}
     (tr : Trace g₁ idx₁ idx₂ ρ₁ ρ₂) :
-    Trace (g₁ ∙ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ := by
-  have h := tr.embed (GGraph.Embed.overlayLeft g₁ g₂)
-  rwa [GGraph.Embed.overlayLeft_f, GGraph.Embed.overlayLeft_f] at h
+    Trace (g₁ ∙ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ :=
+  tr.embed (GGraph.Embed.overlayLeft g₁ g₂)
 
 /-- When two graphs are overlaid, for each trace in the right graph,
     a corresponding trace exists in the combined graph. -/
@@ -56,9 +55,8 @@ noncomputable def Trace.overlay_right {idx₁ idx₂ : g₂.Index}
     a corresponding trace exists in the combined graph. -/
 noncomputable def Trace.sequence_left {idx₁ idx₂ : g₁.Index}
     (tr : Trace g₁ idx₁ idx₂ ρ₁ ρ₂) :
-    Trace (g₁ ⤳ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ := by
-  have h := tr.embed (GGraph.Embed.sequenceLeft g₁ g₂)
-  rwa [GGraph.Embed.sequenceLeft_f, GGraph.Embed.sequenceLeft_f] at h
+    Trace (g₁ ⤳ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ :=
+  tr.embed (GGraph.Embed.sequenceLeft g₁ g₂)
 
 /-- When two graphs are sequenced, for each trace in the second graph,
    a corresponding trace exists in the combined graph. -/