smt: add [smt_inline] operator tag to δ/β-reduce at use sites

[strub]

Higher-order combinators whose body builds a lambda from their own
parameters (e.g. right_loop inv o = forall y, cancel (fun x => o x y) ...) are translated once, polymorphically, into a why3 predicate. The
inner lambdas become polymorphic unamed_lambda symbols, forcing why3's
polymorphism encoding (the uni/sort/t2tb bridges). Discharging a
fully-ground goal like right_loop idfun (^) then requires the prover to
chain several trigger-less higher-order @-apply axioms across that
encoding before it can even case-split — which older SMT solvers fail to
do within the time limit, even though the goal is trivial.

Add a per-operator [smt_inline] tag (mirroring [smt_opaque]): a
fully-applied tagged operator/predicate is δ/β-reduced into the goal
before translation, so its lambdas are created at the call's concrete
instantiation and stay monomorphic — no uni/t2tb detour. Unmarked
definitions are translated exactly as before. The tag is threaded through
the parser, parsetree (pp_tags), scope, and op_opaque.inline, and
consulted by EcSmt.try_inline.

Tag the eight *_loop* combinators in Logic.ec.

Closes #1033.

[oskgo]

This fixes my problem.

I don't like that the solution requires the use of a tag to guide the translation for smt solvers though. I think that unlike smt_opaque this is a much too niche low level implementation detail to expose to users.

You characterise the operators that have this issue as those containing generic lambdas. Would it be possible to automate this heuristic?

Would it be bad for runtime or smt applicability to make all operators (except those that are smt_opaque) use this?

Also, I thought that parametric lemmas were made concrete by instantiating with abstract types? If that's the case, would it be possible to do this abstract monomorphization for the definitional equations as well?