Make Unwind work with some

[mn200]

There's a theorem roughly like

(some x. (x = v) /\ P(x)) = if P(v) then SOME v else NONE

that should be used in the simplifier's unwind technology.

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.

[thtuerk]

I believe the new simple quantifier heuristics, in particular SIMPLE_SOME_INSTANTIATE_CONV implement this.