Ergonomics: Contracts namespace clashes, reserved identifiers (from/to/this), reserved ERC-20 helper names, callee-first ordering

Small ergonomics found while translating ~2500 lines of Solidity into verity_contract on c907fef0:

1. Namespace clashes. emit, typed interface calls (externalStaticCallContractWordsTo, ExternalResult, ExecutableCallContext) are generated as unqualified names from the Contracts namespace, so a contract outside Contracts.* must open Contracts; that makes Int256, toInt256, toUint256, contractAddress, blockTimestamp, blockNumber ambiguous with Verity.* ("Ambiguous term Int256"). Every closure file needs open Contracts hiding Int256 toInt256 toUint256 contractAddress blockTimestamp blockNumber. Generated code should use _root_.Contracts.… qualified names.
2. Reserved identifiers. Solidity parameter names from, to and locals named this, partial fail with parser errors or (for this) a puzzling ExternalResult Uint256 type mismatch, because they are Lean keywords / the anonymous have name. A clear diagnostic ("from is reserved; rename the parameter") would help; ERC-20's _transfer(address from, address to, uint256 amount) is the canonical victim.
3. Reserved helper forms. balanceOf, allowance, totalSupply are ERC-20 helper forms; an ERC-20 contract cannot call its own allowance(owner, spender) internally (the executable rewrite treats it as the helper and produces (fun owner spender => allowance owner_ owner spender) spender type errors).
4. Forward references. Functions must be declared callee-first because the executable plane emits Lean defs in source order; Solidity files are typically ordered the other way.

Closure-side tracking: audit/VERITY-GAPS.md G12/G13/G16.

Start with the G12/G13/G16 entries in audit/VERITY-GAPS.md and reproduce the reported translations from commit c907fef0. Trace generated names, reserved identifiers, ERC-20 helper handling, and executable-plane definition ordering; done means these cases translate without namespace clashes, misleading parser/type errors, helper collisions, or callee-order requirements.