Adopt the convention that axioms and theorems don't have top-level universal quantifiers on the right and existential quantifiers on the left

[SimonGuilloud]

Axiom of extensionality would look like

forall(z, in(z, x) <=> in(z, y)) <=> (x === y)

with x and y free. This makes instantiation more direct and is more consistent with how other schematic symbols are used and presented (as parameters of the theorem or axiom).

[SimonGuilloud]

@lighthea is working on this