P37 Goal laundering

Declarations: P37_stated_goal_not_inferred_goal

From the machine-checked spine in formal/ (core modules are Mathlib-free;Field/Finite/ may import Mathlib). Not self-contained for Lean 4 Web — use the repo or a local lake build.

theorem P37_stated_goal_not_inferred_goal :
    ∃ a b : Bool, ToyStatedGoal a = ToyStatedGoal b ∧ ToyInferredGoal a ≠ ToyInferredGoal b :=
  ⟨true, false, rfl, by decide⟩