Proofgold Proof

pf

Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: In x1 x0.

Apply unknownprop_a5b0141dc7f70dc45c7d1f61b8342a4e97134fda6aab3192ae08a7f3d8c44b7c with λ x2 x3 : ι → ι . In x1 (x3 x0).

Apply unknownprop_1598d20a62a395ced156dfcc7d767ab023594ea6ef7c5e3b53cecdbebaf0ec29 with x0, Repl x0 (λ x2 . (λ x3 . SetAdjoin x3 (Sing 1)) x2), x1.

The subproof is completed by applying H0.

■