diff --git a/Examples/InsulinPump.lean b/Examples/InsulinPump.lean
index 05d7067..7d081c7 100644
--- a/Examples/InsulinPump.lean
+++ b/Examples/InsulinPump.lean
@@ -128,9 +128,7 @@ def requirements : List Requirement := [
   { id := 1, desc := "The controller shall command a bolus within T of CGM readings sustained above threshold",
     ucas := [1, 3] },
   { id := 2, desc := "The controller shall not command insulin when the latest CGM reading is at or below threshold",
-    ucas := [2] },
-  { id := 3, desc := "The controller shall bound each commanded dose and terminate delivery at the commanded amount",
-    ucas := [4] }
+    ucas := [2] }
 ]
 
 /-- STPA step 4 (initial): loss scenarios explaining how each UCA could
@@ -164,16 +162,6 @@ theorem pumpModel_wellFormed : pumpModel.wellFormed = true := by decide
 the controller receives feedback from every process it controls. -/
 theorem pumpCs_wellFormed : pumpCs.wellFormed pumpModel = true := by decide
 
-/-- The full STPA analysis is well-formed: traceable hazards and UCAs, and
-all four UCA kinds covered for every control path. -/
-theorem analysis_wellFormed : analysis.wellFormed = true := by decide
-
-/-- The analysis document is well-typed in the sense of the STPA type
-system (docs/stpa-typesystem.pdf): every artifact well-kinded, every hazard
-addressed by a system constraint, every UCA refined by a controller
-requirement — no orphans. `decide` works on the Prop-level judgment via the
-reflection theorem `Analysis.wellTyped_iff`. -/
-theorem analysis_wellTyped : WellTyped analysis := by decide
 
 -- Round-trip: print the elaborated model back as SysML textual notation.
 -- #sysml pumpModel