Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Apply unknownprop_219a5692ece616b4a88502d80a85b644180cde982b21251f92a23d11d1a5d022 with setsum x0 (binunion x1 x2), binunion (setsum x0 x1) (setsum x0 x2) leaving 2 subgoals.

Let x3 of type ι be given.

Assume H0: In x3 (setsum x0 (binunion x1 x2)).

Apply unknownprop_18583690a94a3aabb1b201c712283c6f832bd4e90b0730d0c8623d2e4a7a992a with x0, binunion x1 x2, x3, λ x4 . In x4 (binunion (setsum x0 x1) (setsum x0 x2)) leaving 3 subgoals.

The subproof is completed by applying H0.

Let x4 of type ι be given.

Assume H1: In x4 x0.

Apply unknownprop_1598d20a62a395ced156dfcc7d767ab023594ea6ef7c5e3b53cecdbebaf0ec29 with setsum x0 x1, setsum x0 x2, Inj0 x4.

Apply unknownprop_1fbfebc9584f3b35fe974f93c7762fab1d5a4f649af5608ad307cbbc36ce4d37 with x0, x1, x4.

The subproof is completed by applying H1.

Let x4 of type ι be given.

Assume H1: In x4 (binunion x1 x2).

Apply unknownprop_a497a9c4fdb392b95b688b10c74f8f445a953a0c88030ccc02fa0b24e4758231 with x1, x2, x4, In (Inj1 x4) (binunion (setsum x0 x1) (setsum x0 x2)) leaving 3 subgoals.

The subproof is completed by applying H1.

Assume H2: In x4 x1.

Apply unknownprop_1598d20a62a395ced156dfcc7d767ab023594ea6ef7c5e3b53cecdbebaf0ec29 with setsum x0 x1, setsum x0 x2, Inj1 x4.

Apply unknownprop_509aadde20bd8e655e679e36fea278577d08a1dbe475eed73f3fccc8c2d65f15 with x0, x1, x4.

The subproof is completed by applying H2.

Assume H2: In x4 x2.

Apply unknownprop_e6919c45bef19e01f88ce072c705412578331e9a3c7532de752ffb4187ed1265 with setsum x0 x1, setsum x0 x2, Inj1 x4.

Apply unknownprop_509aadde20bd8e655e679e36fea278577d08a1dbe475eed73f3fccc8c2d65f15 with x0, x2, x4.

The subproof is completed by applying H2.

Let x3 of type ι be given.

Assume H0: In x3 (binunion (setsum x0 x1) (setsum x0 x2)).

Apply unknownprop_a497a9c4fdb392b95b688b10c74f8f445a953a0c88030ccc02fa0b24e4758231 with setsum x0 x1, setsum x0 x2, x3, In x3 (setsum x0 (binunion x1 x2)) leaving 3 subgoals.

The subproof is completed by applying H0.

Assume H1: In x3 (setsum x0 x1).

Apply unknownprop_18583690a94a3aabb1b201c712283c6f832bd4e90b0730d0c8623d2e4a7a992a with x0, x1, x3, λ x4 . In x4 (setsum x0 (binunion x1 x2)) leaving 3 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying unknownprop_1fbfebc9584f3b35fe974f93c7762fab1d5a4f649af5608ad307cbbc36ce4d37 with x0, binunion x1 x2.

Let x4 of type ι be given.

Assume H2: In x4 x1.

Apply unknownprop_509aadde20bd8e655e679e36fea278577d08a1dbe475eed73f3fccc8c2d65f15 with x0, binunion x1 x2, x4.

Apply unknownprop_1598d20a62a395ced156dfcc7d767ab023594ea6ef7c5e3b53cecdbebaf0ec29 with x1, x2, x4.

The subproof is completed by applying H2.

Assume H1: In x3 (setsum x0 x2).

Apply unknownprop_18583690a94a3aabb1b201c712283c6f832bd4e90b0730d0c8623d2e4a7a992a with x0, x2, x3, λ x4 . In x4 (setsum x0 (binunion x1 x2)) leaving 3 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying unknownprop_1fbfebc9584f3b35fe974f93c7762fab1d5a4f649af5608ad307cbbc36ce4d37 with x0, binunion x1 x2.

Let x4 of type ι be given.

Assume H2: In x4 x2.

Apply unknownprop_509aadde20bd8e655e679e36fea278577d08a1dbe475eed73f3fccc8c2d65f15 with x0, binunion x1 x2, x4.

Apply unknownprop_e6919c45bef19e01f88ce072c705412578331e9a3c7532de752ffb4187ed1265 with x1, x2, x4.

The subproof is completed by applying H2.

■

Proofgold Proof