fix(proofs): add 8 step rules, prove T_Eq progress, document root cause

Added step rules for complete coverage of value forms:
- S_Eq_True_Array, S_Eq_False_Array: array equality via value_eq_dec
- S_Eq_False_LitArray, S_Eq_False_ArrayLit: cross-form inequality
- S_BinOp_Right_Array: reduce right operand with array on left
- S_BinOp_Error_Left_Array, S_BinOp_Error_Right_Array: error propagation
- S_Okay_Error, S_Oops_Error: VOops propagation through wrap/unwrap

T_Eq progress case now has complete proof (was bare admit): all 8 value
constructors handled with value_eq_dec, ELit-EArray cross handled by new
rules, error cases use S_BinOp_Error_Left/Right.

3 Admitted remain — all root-caused to same issue: is_value EArray
requires `map ELit vs` form, but nested arrays produce EArray (not ELit).
Fix requires value representation change (flatten VArray to ELit form).

Compiles clean with coqc 8.20.1.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: hyperpolymath