P28 Missing invariant blocks safety

Declarations: P28_missing_cci_blocks_successor_safety

From the machine-checked spine in formal/ (Mathlib + spine imports). Not self-contained for Lean 4 Web — use the repo or a local lake build.

theorem P28_missing_cci_blocks_successor_safety
    {A B : System}
    (h : ¬ CCIPreserved A B) :
    ¬ SuccessorSafe A B := by
  intro ⟨w⟩
  exact h w.cci