There are antecedents.

You can have a look at https://github.com/coq-contribs/cats-in-zfc (the first files are in order axioms.v tactics.v and set_theory.v, read tactics.v just to know what the tactics in the others mean). The pdf in that repo looks like it’s broken, get it from https://arxiv.org/abs/math/0410224 instead.

Years ago I played around with it and made it more axiomatic (eg instead of `Definition E := Type.`

for the type of sets I have `Axiom E : Type.`

, so you have to use the ZF axioms on it instead of inductive types etc), you can have a look at https://github.com/SkySkimmer/ZF (quality not guaranteed, doesn’t compile with current Coq).

Also, I can’t find a way to prove last theorem named ‘subset_of_singleton’. Is it because I’m not clever enough or maybe I have made a mistake somewhere before? Thanks in advance.

You have excluded middle (classical logic) so you can ask whether `{a}`

belongs to `x`

. The answer lets you know if `x`

is supposed to be empty or `{{a}}`

. Proceed from there.

BTW consider using more informative theorem names than `E1214`

or `T3`

.