Cardano Updates

Compose the force/delay chain with (.) instead of mixing ($) and parens,
and lay the mkInlinePurityTest argument out across lines. Same term.

In an Agda certificate, all work for type-checking the translation relation proofs is done in the top-level agda module. This PR instead constructs a module per pass which has the corresponding translation relation proof. This is useful for performance debugging when type-checking an agda certificate, as we can see a break-down of the decision procedure's performance.

So in addition to Pass_xyz/AST.agda, there is now also Passxyz/Proof.agda. The top-level module simply imports the proofs and constructs the certificate proof (a big tuple).

Replace raw UPLC constructors and the per-arity fresh-name plumbing in the Simplify, Inline, CaseOfCase and EvaluateBuiltins specs with the shared Transform.Lib helpers. Golden outputs are unchanged.

Shared UPLC term builders for the Transform.*.Spec modules: var "x" / lam "x" for occurrences and binders, name "x" for the bare Name, the ite helper, and the sopTrue/sopFalse vs builtinTrue/builtinFalse boolean constants. Variable identity is derived deterministically from the hint text; see Note [Names from textual hints].

Replace raw UPLC constructors and the per-arity fresh-name plumbing in the Simplify, Inline, CaseOfCase and EvaluateBuiltins specs with the shared Transform.Lib helpers and the var.x / lam.x / name.x dot syntax. Golden outputs are unchanged.

Shared UPLC term builders for the Transform.*.Spec modules: var.x and lam.x occurrence/binder handles via OverloadedRecordDot, name.x for bare names, the ite helper, and the sopTrue/sopFalse vs builtinTrue/builtinFalse boolean constants. Variable identity is derived deterministically from the hint text, so one hint denotes one variable.

Rename true/false to sopTrue/sopFalse (the sum-of-products Bool encoding) and add
builtinTrue/builtinFalse (the builtin bool constant), so the two encodings are
named explicitly. Add an `ite` helper for the forced ifThenElse application and
use it across the CaseOfCase, EvaluateBuiltins and Simplify specs, dropping the
local `ite` in Simplify.

Replace raw constructors with the shared helpers (app, builtin, force, case_,
con, text, constr, true, false, err) and chained `app` for mkIterApp, in the two
modules that already import Transform.Lib. Only mkConstant @Bool / @() /
@BS.ByteString stay raw, as Lib has no equivalent (con/text cover Integer/Text).

Replace raw `Var () name.x` / `LamAbs () name.x` with the var.x / lam.x handles
for consistency with the other transform specs. These modules keep their raw
constructors for the non-variable parts (mkIterApp, Force, Builtin, Constr).

The bare-Name handle does not allocate fresh names; it derives a deterministic
Unique from the hint text, so `name.x` reads more accurately than `fresh.x`
(addresses review feedback). Rename the goldenVs* test-name params to testName
to avoid shadowing the imported handle.

Turn var and lam into OverloadedRecordDot handles (var.x :: T, lam.x :: T -> T)
so occurrences and binders read as var.x / lam.x instead of var fresh.x. Bare
names (predicate args, free-var lists, raw-constructor modules) still come from
the fresh handle. Drop the now-redundant brackets and $ that hlint flagged.