Require (or at least allow) witnesses for choose

[vkuncak]

Choose construct is used internally in Stainless as well as exposed to the user. However, soundness of choose depends on the conjunction of the type and the predicate being non-empty. The proof obligation for this is in fact a quantified statement, which breaks the design principle that core functionality should not require quantifiers.

I thus propose that we introduce explicitly provided witnesses for choose, so that we eliminate the need for quantifiers.

choose((x:T) => p, witness)

would check witness:T (however that should be represented in the SystemFR type checker) and then check

assert(p(witness))

[vkuncak]

For abstract methods, instead of using ???, let us introduce ???(w) where w specifies a witness value.

[vkuncak]

I would like a solution that in most of our current cases avoids the need for solving quantified constraints. @samarion we may need your opinion as it seems to be affecting core of Inox.