diff --git a/lean/Spa/Language/Properties.lean b/lean/Spa/Language/Properties.lean
index 28ccba0..5ebfa67 100644
--- a/lean/Spa/Language/Properties.lean
+++ b/lean/Spa/Language/Properties.lean
@@ -198,21 +198,38 @@ noncomputable def EndToEndTrace.loop_empty {ρ : Env} : EndToEndTrace (Graph.loo
 
 end Loop
 
-/-! ### Singletons, wrap, and the main result -/
-
+/-- A CFG consisting of only a single node has a trace through it corresponding to that node. -/
 noncomputable def EndToEndTrace.singleton {o : Option BasicStmt} {ρ₁ ρ₂ : Env}
     (h : EvalBasicStmtOpt ρ₁ o ρ₂) : EndToEndTrace (Graph.singleton o) ρ₁ ρ₂ :=
   ⟨(0 : Fin 1), List.mem_singleton_self _, (0 : Fin 1), List.mem_singleton_self _,
    Trace.single h⟩
 
+/-- If a CFG's only node is empty, the no-op trace exists through it. -/
 noncomputable def EndToEndTrace.singleton_nil (ρ : Env) :
     EndToEndTrace (Graph.singleton none) ρ ρ :=
   EndToEndTrace.singleton EvalBasicStmtOpt.none
 
+/-- Invoking 'Graph.wrap` (which ensures a single entry and exit node for a CFG)
+    does not invalidate traces in the original graph. -/
 noncomputable def EndToEndTrace.wrap {g : Graph} {ρ₁ ρ₂ : Env}
     (etr : EndToEndTrace g ρ₁ ρ₂) : EndToEndTrace (Graph.wrap g) ρ₁ ρ₂ :=
   (EndToEndTrace.singleton_nil ρ₁).concat (etr.concat (EndToEndTrace.singleton_nil ρ₂))
 
+/-- Key result: the control flow graph admits every execution that's made
+    possible by a language's semantics. Thus, the CFG encodes _at least_ all
+    semantically-possible executions. Informally, we can conclude from this
+    that if we compute a result that using the graph's edges to determine
+    what's possible, this result will not disagree with the semantics.
+
+    Note that a CFG like $K_4$ (where the nodes are basic blocks) is
+    technically also a sufficient graph, but is very likely meaningless in that
+    it grossly overestimates the possible execution paths in the language, and
+    thus is bound to produce less-than-specific results. There is as yet no
+    result in this framework that the CFG we produce is _minimal_: loosely,
+    posessing only edges for things that are admitted by the semantics.
+    This is difficult to state (in its strongest form, this would
+    require the CFG to be able to detect something like `while (alwaysFalse)`,
+    and so remains a TODO. -/
 noncomputable def Stmt.cfg_sufficient {s : Stmt} {ρ₁ ρ₂ : Env}
     (h : EvalStmt ρ₁ s ρ₂) : EndToEndTrace s.cfg ρ₁ ρ₂ := by
   induction h with
@@ -229,20 +246,24 @@ noncomputable def Stmt.cfg_sufficient {s : Stmt} {ρ₁ ρ₂ : Env}
   | whileFalse ρ e s _ =>
     exact EndToEndTrace.loop_empty
 
-/-! ### The wrapped graph's entry has no predecessors (Agda's "ugly" block) -/
-
+/-- The input / entry node generated by `Graph.wrap`. -/
 def Graph.wrapInput (g : Graph) : (Graph.wrap g).Index :=
   (0 : Fin 1).castAdd ((g ⤳ Graph.singleton none).size)
 
+/-- The output / exit node generated by `Graph.wrap`. -/
 def Graph.wrapOutput (g : Graph) : (Graph.wrap g).Index :=
   Fin.natAdd 1 ((Fin.natAdd g.size (0 : Fin 1)))
 
+/-- The `Graph.wrapInput` is, indeed, the graph's only input after `Graph.wrap`. -/
 lemma Graph.wrap_inputs (g : Graph) :
     (Graph.wrap g).inputs = [g.wrapInput] := rfl
 
+/-- The `Graph.wrapInput` is, indeed, the graph's only output after `Graph.wrap`. -/
 lemma Graph.wrap_outputs (g : Graph) :
     (Graph.wrap g).outputs = [g.wrapOutput] := rfl
 
+/-- When sequencing (proven here with `Graph.singleton` on the left), no edges
+    exist from the right-hand graph back to the left. -/
 private lemma not_mem_edges_castAdd_sequence {g₂ : Graph} (i : Fin 1)
     (idx : (Graph.singleton none ⤳ g₂).Index) :
     ((idx, i.castAdd g₂.size) : (Graph.singleton none ⤳ g₂).Edge)
@@ -260,6 +281,7 @@ private lemma not_mem_edges_castAdd_sequence {g₂ : Graph} (i : Fin 1)
     obtain ⟨j, -, heq⟩ := List.mem_map.mp hb
     exact Fin.castAdd_ne_natAdd i j heq.symm
 
+/-- The input node of a graph after `Graph.wrap` has no predecessors. -/
 lemma Graph.wrap_predecessors_eq_nil (g : Graph) (idx : (Graph.wrap g).Index)
     (h : idx ∈ (Graph.wrap g).inputs) :
     (Graph.wrap g).predecessors idx = [] := by