Simon Cruanes

in `Elim_multi_eqns`, emit warning if some cases are undefined (and print corresponding input pattern)

transform `exists x. y = s x & p[x]` into `is-s y && p[select-s-0 y]` note: would apply to backends CVC4 and smbc, at least?

- no universes - must be accepted in typechecking (without inference for term parameters) - do the encoding (hatt 2016)

transformation for inlining non-recursive defined functions

in encoding of functions, add the prototype (perhaps with a flag to enable/disable it).

call CVC4 with `--fmf-empty-sorts` to avoid refining recursive functions that are not used. We need to force it to fill other sorts though, by declaring `p : sort -> bool`,...

A call to simple.solve seems to take an arbitrary amount of time in tracing. Spends its time doing pivots. It might be a problem with epsilons? repro: ```sh $ /sidekick.sh...

an array.sort/bigarray.sort (perhaps functorized) that works in-place on slices would be super useful as we use sort a lot in the SAT solver.