Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H0: x2binunion x0 x1.
Apply UnionE_impred with UPair x0 x1, x2, or (x2x0) (x2x1) leaving 2 subgoals.
The subproof is completed by applying H0.
Let x3 of type ι be given.
Assume H1: x2x3.
Assume H2: x3UPair x0 x1.
Apply UPairE with x3, x0, x1, or (x2x0) (x2x1) leaving 3 subgoals.
The subproof is completed by applying H2.
Assume H3: x3 = x0.
Apply orIL with x2x0, x2x1.
Apply H3 with λ x4 x5 . x2x4.
The subproof is completed by applying H1.
Assume H3: x3 = x1.
Apply orIR with x2x0, x2x1.
Apply H3 with λ x4 x5 . x2x4.
The subproof is completed by applying H1.