perf(cbv): cache operator instances and closed-term normal forms

[strub]

Computation-heavy proofs spent most of their time redoing work that is
invariant across a single norm_cbv run:

• every delta-unfolding re-instantiated the operator body with
  Tvar.f_subst ~freshen:true, and every fix step additionally re-ran
  form_of_expr on the selected branch;
• operator classification (is_dtype_ctor, is_projection, ...) redid a
  by-path environment lookup at every node;
• closed applications (table lookups, powers, word constants) were
  re-evaluated from scratch at every occurrence.

Add per-run caches for all three, keyed respectively by (path, tys),
(path, tys, ctor indices), by path, and - for the normal-form cache -
by the hash-consed application itself, guarded by an empty f_fv so that
nothing context-dependent is memoized. Within one norm_cbv run the
environment, hypotheses and reduction_info are fixed, so the result of
reducing a term without free local, memory or module identifiers is a
pure function of the term. Sharing one freshened body across unfoldings
is sound because cbv substitutions are capture-avoiding.

On the goldbach pre-sieve table proofs (5957 bytes checked bit by bit)
the second cbv goal drops from 22.2s to 2.2s; a bare 8-byte table
lookup per bit drops from 330us to a table hit.