proof

Access non-id.

Lean spine source

Declarations: access_equivalence_nonidentifiability

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 access_equivalence_nonidentifiability
    {A : AccessModel} {M₁ M₂ : Model}
    (heq : AccessEquivalent A M₁ M₂)
    (hgoal : ModelGoal M₁ ≠ ModelGoal M₂) :
    ¬ IdentifiableFromAccess A ModelGoal := by
  intro hId
  exact hgoal (hId M₁ M₂ heq)