The discussion in #1600 shows that the {ae mu, P} notation is used in places where \forall x \ae mu, Q x should be preferred (where P = forall x, Q x).
We should review all instances of ae and near to check that {ae and {near are used only when an existing statement is being relativised. Otherwise prefer \forall x \ae mu and \forall x \near F, respectively.
Additionally, we should consider equivalent notation for in (i.e. introduce \forall x \in D, P x to match the {in D, P} notation and check all instances).
The discussion in #1600 shows that the
{ae mu, P}notation is used in places where\forall x \ae mu, Q xshould be preferred (whereP = forall x, Q x).We should review all instances of
aeandnearto check that{aeand{nearare used only when an existing statement is being relativised. Otherwise prefer\forall x \ae muand\forall x \near F, respectively.Additionally, we should consider equivalent notation for
in(i.e. introduce\forall x \in D, P xto match the{in D, P}notation and check all instances).