STを使ってFalseを示す例

If you're curious, here's a proof of False using ST.Ref.get:

```lean4
def test : ST ω Nat := fun s =>
  let ⟨ref, s₁⟩ := ST.Prim.mkRef 0 s
  let ⟨n, _⟩ := ST.Prim.Ref.get ref s₁
  let ⟨(), s₃⟩ := ST.Prim.Ref.set ref 1 s₁
  ⟨n, s₃⟩

def test2 : ST ω Nat := fun s =>
  let ⟨ref, s₁⟩ := ST.Prim.mkRef 0 s
  let ⟨(), s₃⟩ := ST.Prim.Ref.set ref 1 s₁
  let ⟨n, _⟩ := ST.Prim.Ref.get ref s₁
  ⟨n, s₃⟩

example : False := by
  have : (test (Void.mk ())).1 = 0 := by native_decide
  have : (test2 (Void.mk ())).1 = 1 := by native_decide
  have : @test = @test2 := rfl
  simp_all
```

Start by reproducing the code block with ST.Prim.mkRef, ST.Prim.Ref.get, ST.Prim.Ref.set, and native_decide in the repository's example environment. Check whether the claimed definitional equality between test and test2 is valid and identify what the example demonstrates. Done means the reported contradiction is explained and the affected example or documentation is resolved.