Proofgold Proof

pf
Let x0 of type ι be given. Let x1 of type ι be given. Assume H0: In x1 (Sing x0). Assume H1: x1 = x0 ⟶ False. Apply H1. Apply unknownprop_5b60b98e3f1eb090f9a13c5f00bc0b9619444831e46991a07d9b3c034c70e912 with x0, x1. The subproof is completed by applying H0. ■