fix(subst): also bind expression-locals when substituting a form-local (#1056)

[bgregoir]

When a quantified variable in a lemma statement is instantiated (e.g. apply (eager_f_sample z) substituting y -> z), the substitution only updated the form-level locals. Variables embedded inside program statements carried by the formula -- the s1/s2 bodies of an eager [...] judgement, for instance -- live as expression-level locals and were left untouched, producing an incorrect statement substitution.

In both substitution engines (ecCoreSubst.f_bind_local and ecSubst.add_flocal), when binding a form-local x |-> t, if t is translatable back to an expression we now also register the corresponding expression-local binding (bind_elocal / add_elocal). Forms that don't translate (CannotTranslate) are left as before.

tests/eager_call_instanciate.ec reproduces the bug and now passes.

Partially address #1056

[bgregoir]

I suspect that the function EcSubst.add_flocal also has a similar problem

[strub]

@bgregoir By ignoring the CannotTranslate exception, this is half-solving the bug. But I suspect that if we do not ignore it, we are going to have a lot of regression. The real fix is not get rid of expressions once and for all, something that is out of scope of this PR.

In consequence, issue #1056 won't be closed by this PR.