Profiling reflective decide: measure formula sizes in compiled code first

When a reflective decide +kernel proof is slow, write a tiny elab command that reifies the goal, evalExprs the AST, and prints the size of the intermediate results of each step in compiled code (unsafe evalExpr MyAST (mkConst MyAST) e; call synthesizeSyntheticMVarsNoPostponing after elabTerm or numeral instances stay as mvars). This told me in seconds whether the cost was blowup (Cooper QE: 557-node intermediates) or kernel overhead. Also: when timing test lines one by one, re-derive the line numbers after every edit; I spent a while optimising the wrong example. Cheap fix for QE blowup: split the body into DNF and distribute the existential over the disjuncts, but guard with a numeric disjunct count (or: a+b, and: a*b). Checking (dnf φ).length builds the exponential list and hung.