"exists" instead "EXType"

[georgydunaev]

I think that it is common now to use "exists" instead "EXType". Shall I rename it in the whole repository?
It is also possible to use "Defined." instead of "Qed."
https://gmalecha.github.io/reflections/2017/qed-considered-harmful
Will it be approved?

[herbelin]

I think that it is common now to use "exists" instead "EXType". Shall I rename it in the whole repository?

Yes, it will be approved.

It is also possible to use "Defined." instead of "Qed."

This question is more controversial. In a work like zfc where things do not compute a lot, I suspect that it does not matter so much, but in the general case, there is dilemma between ability to compute and ability to abstract. In practice, we may want one or the other depending on situation.

If you have a practical motivation for moving some statements to Defined, that will be approved. If it is just as an informal experiment w/o real need, I would lean towards staying with Qed.