PrecondElim swaps de Bruijn indices in WF obligations under nested quantifiers

[joscoh]

PrecondElim swaps de Bruijn indices in WF obligations under nested quantifiers

Bug

Lambda.collectWFObligations (Strata/DL/Lambda/Preconditions.lean), run by the
PrecondElim phase, mis-scopes an accumulated hypothesis when it is carried
across a quantifier introduced deeper in the traversal.

At a &&, the left conjunct is pushed onto implications as a hypothesis:

else if opName == (@boolAndFunc T).name then
  let lhsObs := go F lhs implications
  let rhsObs := go F rhs ((md, lhs) :: implications)   -- lhs captured at current depth
  lhsObs ++ rhsObs

If the right conjunct introduces a new binder (a nested quantifier), the
captured lhs is later emitted under that new binder, but its dangling bvars
are never lifted. wrapImplications does a plain foldr with no index shift.
Result: the hypothesis's bound-variable references are captured by the wrong
binder — the two bound variables get swapped.

Consequence downstream: PrecondElim runs before type checking, so the
malformed obligation is then type-checked and fails with e.g.
Impossible to unify (arrow Inner Outer) with (arrow int $__ty0).

Test case (run, passes — pins the transform output)

StrataTest/Languages/Core/Examples/PrecondElimNestedQuantBug.lean runs
only PrecondElim (no type checking) and prints the result:

function bug(p: Outer): bool {
  exists m: Inner :: p == Outer_A(m) && (exists j: int :: Inner..x(m) == j)
}

The generated obligation (matched by #guard_msgs, build is green):

assert [bug_body_calls_Inner..x_0]:
  forall m : Inner :: forall j : int :: p == Outer_A(j) ==> Inner..isInner_Cons(m);

It should be ... p == Outer_A(m) ==> Inner..isInner_Cons(m). m : Inner and
j : int are swapped, so Outer_A : Inner -> Outer is applied to the
int-typed j.

Proposed fix

When entering a binder during traversal, lift the dangling bvars of every
already-accumulated implication by 1 using the existing Lambda.liftBVars
(Strata/DL/Lambda/LExprWF.lean). In the .quant (and .abs) case of
collectWFObligations.go:

| .quant md _ name ty trigger body =>
  let implications := implications.map (fun (m, h) => (m, Lambda.liftBVars 1 h))
  (go F body implications).map fun ob =>
    { ob with obligation := .quant md .all name ty trigger ob.obligation }

This keeps each hypothesis's free bvars pointing at their original binders after
the extra quantifier is interposed. After the fix the obligation reads
Outer_A(m) and the example verifies.