The proof would be by induction (much like http://us2.metamath.org/ileuni/nn0suc.html ). It would be stated something like ( A e. om /\ B e. Om ) -> ( A = B \/ -. A = B ) (or the equivalent using DECID).
I have removed the good first issue label (although the trickiness is more in the math than in how the formalization works). Proving A e. om -> ( A = (/) \/ -. A = (/) by induction is easy (see nndc in #728 ), but going from there to A e. om -> ( A = B \/ -. A = B would seem to have different cases. From (/) up to before A we'd would hit the -. A = B half, and then one which hits the A = B half, and then -. A = B again. When stated like that, it sounds like the kind of case elimination which doesn't work in intuitionistic logic. There should be a way to fix this, although it might involve < or + or some other trick which requires some preliminary development.
This is in iset.mm.
The proof would be by induction (much like http://us2.metamath.org/ileuni/nn0suc.html ). It would be stated something like
( A e. om /\ B e. Om ) -> ( A = B \/ -. A = B )
(or the equivalent usingDECID
).I have removed the
good first issue
label (although the trickiness is more in the math than in how the formalization works). ProvingA e. om -> ( A = (/) \/ -. A = (/)
by induction is easy (seenndc
in #728 ), but going from there toA e. om -> ( A = B \/ -. A = B
would seem to have different cases. From(/)
up to beforeA
we'd would hit the-. A = B
half, and then one which hits theA = B
half, and then-. A = B
again. When stated like that, it sounds like the kind of case elimination which doesn't work in intuitionistic logic. There should be a way to fix this, although it might involve<
or+
or some other trick which requires some preliminary development.