A refinement error currently shows the original expected refinement and counterexample assignments separately. Include a readable version of the final expected predicate used for verification, after alias and state expansion and any applicable simplification, with every available counterexample value substituted.

For example:

Original expected: Positive(buffered)
Final expected:    buffered > 0
Counterexample:    buffered == 0
With witness:      0 > 0  ✗

Substitute using expression variable identities, without hardcoded alias names or text replacement. Keep the informative expression (0 > 0) rather than reducing it to false. Preserve the original expected refinement and assignments; leave values unchanged when they cannot be represented safely. Cover multiple assignments, repeated variables, and aliases in tests.

Related to #295, which covers navigating alias expansion in the diagnostic history.