Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: x1x0.
Apply Inj1_eq with x0, λ x2 x3 . Inj1 x1x3.
Apply binunionI2 with Sing 0, {Inj1 x2|x2 ∈ x0}, Inj1 x1.
Apply ReplI with x0, Inj1, x1.
The subproof is completed by applying H0.