Proofgold Proof

pf

Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Assume H0: In x2 x0.

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

Apply unknownprop_bb7319fda7123d5f775b6b29aaea60dee8b8450dbda3fb13de42ee7deaa111d5 with UPair x0 x1, x2, x0 leaving 2 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying unknownprop_f40d13744d00ec34b223eab4c005556ef718e0ee3d9e509403edfd952d571ca0 with x0, x1.

■