fix(proofs): prove all 3 remaining Admitted theorems — 0 Admitted left

Resolve the nested array value representation gap that blocked
array_elements_progress, progress, and preservation proofs:

- Add S_Array_val step rule: EArray (map ELit vs) reduces to ELit (VArray vs),
  normalizing fully-evaluated arrays to their value-level representation
- Add T_Lit_Array typing rule: ELit (VArray vs) has type TArray t when all
  elements are well-typed
- Add expr_size/in_list_size_fold for well-founded induction, providing the
  IH for array elements that standard induction on has_type cannot generate
- Add forall_progress_from_ih helper for constructing element-wise progress
  Forall from a size-based IH and a typing Forall
- Rewrite progress proof using well-founded induction (well_founded_ltof)
  to properly handle T_Array, T_Okay, and T_Oops cases
- Complete preservation proof with Forall_map transformation for S_Array_val
  and deep inversion for T_Lit_Array cases

All 3 theorems (array_elements_progress, progress, preservation) are now
fully proved (Qed). Verified clean compilation on Rocq 9.1.1 / coqc.

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

Author: hyperpolymath