fix(fixpoint): matchfix termination check must descend into all call arguments

[namasikanam]

Summary

The structural-recursion (termination) check for op ... with ... fixpoint definitions accepts
a non-well-founded operator, because it does not descend into all arguments of a recursive
call. This lets one define f x = ¬ f x, which has no total-function solution and makes the
theory inconsistent.

Reproducer (accepted on current main)

type t = [ Z | S of t ].
op f (n : t) (b : bool) : bool =
  with n = Z   => b
  with n = S k => f k (! (f n b)).

easycrypt compile accepts this. The outer call f k (…) decreases on k (a subterm of
S k), so the guard accepts it and never inspects the sibling argument ! (f n b), which
recurses on the whole input n (non-decreasing). The defining equations give
f (S Z) b = f Z (¬ f (S Z) b) = ¬ f (S Z) b, i.e. X = ¬X — inconsistent.

(Note: extracting a literal .ec proof of false is blocked because EC's normalizer loops on
the self-referential reduct; but accepting the definition is already the soundness break — no
total function f satisfies these equations. A control with the bad call placed directly, not
hidden in a valid call's argument, is correctly rejected.)

Root cause

trans_matchfix's check_body (ecHiInductive.ml), on finding a recursive call whose
decreasing-position argument is a valid structural subterm, returns () without checking
the call's other arguments — so a non-decreasing recursive call hidden in a sibling argument
escapes.

Fix

Descend into all arguments of an accepted recursive call
(-> List.iter check_body args). Legitimate recursion — including nested decreasing sibling
calls like f k (f k b) — is unaffected.

Validation

• Bad definition rejected; good/nested-decreasing definitions still accepted.
• Full stdlib (128/128) + examples + unit: clean.
• Regression test tests/matchfix-termination.ec (fail op …).