Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_55ac2036b2594a1420c3213980e6cc84263d48ba5c2b4b8c0dc5b53adbf2cdcc with ZermeloWO x0, ZermeloWO x1, or (ZermeloWO x0 x1) (ZermeloWO x1 x0) leaving 4 subgoals.
The subproof is completed by applying unknownprop_1c5184f86aa281587f2541b20dafbf0fb59ed16c97a848ba15b898cfd0b2908e with x0.
The subproof is completed by applying unknownprop_1c5184f86aa281587f2541b20dafbf0fb59ed16c97a848ba15b898cfd0b2908e with x1.
Assume H0: ∀ x2 . ZermeloWO x1 x2 ⟶ ZermeloWO x0 x2.
Apply orIL with ZermeloWO x0 x1, ZermeloWO x1 x0.
Apply H0 with x1.
The subproof is completed by applying ZermeloWO_ref with x1.
Assume H0: ∀ x2 . ZermeloWO x0 x2 ⟶ ZermeloWO x1 x2.
Apply orIR with ZermeloWO x0 x1, ZermeloWO x1 x0.
Apply H0 with x0.
The subproof is completed by applying ZermeloWO_ref with x0.
■