Executable semantic helpers

Fuel monotonicity for the Nat-level evalN reference.

theorem Nock.evalN_succ {n : Nat} {s form r : Noun} (h : evalN n s form = some r) : evalN (n + 1) s form = some r

theorem Nock.evalN_mono {n m : Nat} {s form r : Noun} (hle : n ≤ m) (h : evalN n s form = some r) : evalN m s form = some r

theorem Nock.evalN_deterministic {n m : Nat} {s form r₁ r₂ : Noun} (h₁ : evalN n s form = some r₁) (h₂ : evalN m s form = some r₂) : r₁ = r₂

evalN is a partial function (output uniqueness). Two successful evaluations of the same subject/formula, at any fuel budgets, return the same noun. Fuel controls only whether evaluation finishes, never the result. Proof: bump both to the common fuel max n m by evalN_mono, then some is injective.