Proofgold Proof

pf
Let x0 of type ι be given. Let x1 of type ι be given. Let x2 of type ι be given. Assume H0: x2 ∈ x1. Apply binunionI2 with {Inj0 x3\|x3 ∈ x0}, {Inj1 x3\|x3 ∈ x1}, Inj1 x2. Apply ReplI with x1, Inj1, x2. The subproof is completed by applying H0. ■