z_%exists%_intro and z_%exists%_elim

[rbjones]

Though rules for introduction and elimination of universal quantifiers specific to z exist, the corresponding ones for existential quantifiers don't exist.

[RobArthan]

I'll have a look into this. It might be a good test case for transferring fixes and enhancements from pp to pp-utf8 (or pp2020, should I say?).

[rbjones]

What say we assign this to copilot and see what it comes up with? Probably best on the utf8 branch so the ext codes don't confuse it. (I don't expect it to work but might be interesting to see how it does, it will only come up with a pull request so we can ditch it).

[RobArthan]

I don't understand who or what you mean by "copilot".

[rbjones]

Microsoft calls its integrated LLM's copilot, and owns GitHub, so Github's AI is called copilot.
This is rapidly advancing area, moving from interactive code completion (and "vibe coding") not so long ago to the possibility of copilot contributing to a project in a manner very similar to human project members, being assigned tasks which might last days or weeks, writing or amending code, and tests, running tests checking the results and amending the code appropriately until eventually making a pull request with the results.