Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: Inj0 x0 = Inj1 x1.
Claim L1: 0Inj1 x1
The subproof is completed by applying Inj1I1 with x1.
Claim L2: 0Inj0 x0
Apply H0 with λ x2 x3 . 0x3.
The subproof is completed by applying L1.
Apply Inj0E with x0, 0, False leaving 2 subgoals.
The subproof is completed by applying L2.
Let x2 of type ι be given.
Assume H3: and (x2x0) (0 = Inj1 x2).
Apply Inj1NE1 with x2.
Let x3 of type ιιο be given.
Apply andER with x2x0, 0 = Inj1 x2, λ x4 x5 . x3 x5 x4.
The subproof is completed by applying H3.