Let x0 of type ι be given.

Apply unknownprop_1b764290fde7c6be5dad24a6a257b6d0c773613bb687261020b529743ed07853 with x0, setsum x0 0.

Apply unknownprop_4b95783dcb3eee1943e1de5542f675166ef402c8fbdda80bdf0920b55d3fc6de with x0, setsum x0 0, Inj0.

Apply unknownprop_aa42ade5598d8612d2029318c4ed81646c550ecc6cdd9ab953ce4bf73f3dd562 with x0, setsum x0 0, Inj0 leaving 2 subgoals.

The subproof is completed by applying unknownprop_191ba52f7596eac3c13199d06abc28bd67d9baab59edf519e02ad968d3f37956 with x0, 0.

Let x1 of type ι be given.

Assume H0: In x1 (setsum x0 0).

Apply unknownprop_18583690a94a3aabb1b201c712283c6f832bd4e90b0730d0c8623d2e4a7a992a with x0, 0, x1, λ x2 . ∃ x3 . and (In x3 x0) (Inj0 x3 = x2) leaving 3 subgoals.

The subproof is completed by applying H0.

Let x2 of type ι be given.

Assume H1: In x2 x0.

Let x3 of type ο be given.

Assume H2: ∀ x4 . and (In x4 x0) (Inj0 x4 = Inj0 x2) ⟶ x3.

Apply H2 with x2.

Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with In x2 x0, Inj0 x2 = Inj0 x2 leaving 2 subgoals.

The subproof is completed by applying H1.

Let x4 of type ι → ι → ο be given.

Assume H3: x4 (Inj0 x2) (Inj0 x2).

The subproof is completed by applying H3.

Let x2 of type ι be given.

Assume H1: In x2 0.

Apply FalseE with ∃ x3 . and (In x3 x0) (Inj0 x3 = Inj1 x2).

Apply unknownprop_1cc88f7e87aaf8c5cee24b4a69ff535a81e7855c45a9fd971eec05ee4cc28f9c with x2.

The subproof is completed by applying H1.

■

Proofgold Proof