Add Axiom of e.-induction to iset.mm
Add Axiom of e.-induction to iset.mm

This is our replacement for the Axiom of Regularity.

As explained in Crosilla, regularity implies undesirable forms
of the law of the excluded middle.

We don't yet have anything proved from e.-induction, but
once we figure out well-foundedness (or proofs directly
from e.-induction), we may be able to bring in some of
the theorems which had been using regularity (and/or
some of the ones proved without regularity in set.mm
but which we don't have yet in iset.mm).

metamath/set.mm,metamath/set.mm,metamath/set.mm