strategy: `instantiate-universals`

[h0nzZik]

Can we instantiate universal variables with any patterns, or the pattern needs be functional? In the latter case, we need to add a parameter by[Strategies] containing strategies for proving the functionality of a pattern - and we need to add such strategies.

[h0nzZik]

The pattern needs to be functional, otherwise we could from the axiom \forall x. \exists y. x = y prove that exists y. (1 \/ 2) = y, which is not true. So how do we check that it is functional? Currently, the prover has no support for checking functionality, except that thesmt` strategies work with functional symbols.

[h0nzZik]

A straightforward way is to define a function isSurelyFunctional that returns true for Ints and application of functional symbols to functional patterns.

[nishantjr]

A straightforward way is to define a function isSurelyFunctional that returns true for Ints and application of functional symbols to functional patterns.

This seems reasonable. In general anything built from constructors (including Ints) and quantified variables.

[h0nzZik]

@nishantjr This PR is ready to be reviewed.

I propose that we rename this strategy to instantiate-element-variables and extend it to work also with free elemet variables. Eventually, there would exist some instantiate-set-variables counterpart, that would instantiate (necessarily free) set variables to any patterns. I would leave both of this as a future work.