Recursion under quantifier inside of `let function`
I know that we discussed this back in october, but I cannot find any trace of our discussions.
Currently if you define a let rec function
and perform a recursive call under a quantifier, you get an unbound predicate or function
error for namespace reasons.
We had discussed several solutions, but I forget what the tradeoffs were.
cc @x-DEwert who independently stumbled on this.