Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Apply unknownprop_219a5692ece616b4a88502d80a85b644180cde982b21251f92a23d11d1a5d022 with binunion 0 x0, x0 leaving 2 subgoals.
Let x1 of type ι be given.
Assume H0: In x1 (binunion 0 x0).
Apply unknownprop_a497a9c4fdb392b95b688b10c74f8f445a953a0c88030ccc02fa0b24e4758231 with 0, x0, x1, In x1 x0 leaving 3 subgoals.
The subproof is completed by applying H0.
Assume H1: In x1 0.
Apply FalseE with In x1 x0.
Apply unknownprop_1cc88f7e87aaf8c5cee24b4a69ff535a81e7855c45a9fd971eec05ee4cc28f9c with x1.
The subproof is completed by applying H1.
Assume H1: In x1 x0.
The subproof is completed by applying H1.
Let x1 of type ι be given.
Assume H0: In x1 x0.
Apply unknownprop_e6919c45bef19e01f88ce072c705412578331e9a3c7532de752ffb4187ed1265 with 0, x0, x1.
The subproof is completed by applying H0.