eliminate existential quantifier tactic

Stream: new members

[Chris M]

Looking through the docs I somehow can't find a tactic that eliminates an existential quantifier. Is there a tactic for this? The safe tactic does this apparently, but also does lots of other things.

[Johan Commelin]

cases

[Chris M]

oh, thanks!

[Jalex Stark]

have you played through any tutorial material such as the natural number game or #mil?

[Chris M]

Apparently not attentively enough. I'll finish #mil more thoroughly.

[Jalex Stark]

:) of course you can still ask questions here! I'm just worried that there are 10 more proof tricks that you'd pick up by playing through more game levels, but which you wouldn't think to ask about otherwise

[Chris M]

Ah, ok, thanks :)