Let x0 of type ι be given.

Apply unknownprop_90bc64785a62f436436f79ffade2005019961924ea270765e5e2c87d9af3394c with Inj0 x0, λ x1 x2 . x2 = x0.

Apply unknownprop_219a5692ece616b4a88502d80a85b644180cde982b21251f92a23d11d1a5d022 with Repl (setminus (Inj0 x0) (Sing 0)) (λ x1 . Unj x1), x0 leaving 2 subgoals.

Let x1 of type ι be given.

Assume H0: In x1 (Repl (setminus (Inj0 x0) (Sing 0)) (λ x2 . Unj x2)).

Apply unknownprop_89e422bb3b8a01dd209d7f2f210df650a435fc3e6005e0f59c57a5e7a59a6d0e with setminus (Inj0 x0) (Sing 0), Unj, x1, In x1 x0 leaving 2 subgoals.

The subproof is completed by applying H0.

Let x2 of type ι be given.

Assume H1: In x2 (setminus (Inj0 x0) (Sing 0)).

Assume H2: x1 = Unj x2.

Apply unknownprop_e02b92c94ff70655b8eb0623a7ec106c0c0c9c65ac0f52f9689f2e6c9f563b5d with Inj0 x0, Sing 0, x2, In x1 x0 leaving 2 subgoals.

The subproof is completed by applying H1.

Apply unknownprop_8583c67a5354a94a214412f684d3146c279871f65a15e5b831f23231b1641441 with λ x3 x4 : ι → ι . In x2 (x4 x0) ⟶ nIn x2 (Sing 0) ⟶ In x1 x0.

Assume H3: In x2 (Repl x0 (λ x3 . Inj1 x3)).

Assume H4: nIn x2 (Sing 0).

Apply unknownprop_89e422bb3b8a01dd209d7f2f210df650a435fc3e6005e0f59c57a5e7a59a6d0e with x0, Inj1, x2, In x1 x0 leaving 2 subgoals.

The subproof is completed by applying H3.

Let x3 of type ι be given.

Assume H5: In x3 x0.

Assume H6: x2 = Inj1 x3.

Claim L7: x1 = x3

Apply H2 with λ x4 x5 . x5 = x3.

Apply H6 with λ x4 x5 . Unj x5 = x3.

The subproof is completed by applying unknownprop_56702b69fe31029117149136473717807c61136823145112690cf6c5e3fd3b5f with x3.

Apply L7 with λ x4 x5 . In x5 x0.

The subproof is completed by applying H5.

Let x1 of type ι be given.

Assume H0: In x1 x0.

Apply unknownprop_56702b69fe31029117149136473717807c61136823145112690cf6c5e3fd3b5f with x1, λ x2 x3 . In x2 (Repl (setminus (Inj0 x0) (Sing 0)) (λ x4 . Unj x4)).

Apply unknownprop_63c308b92260dbfca8c9530846e6836ba3e6be221cc8e80fd61db913e01bdacf with setminus (Inj0 x0) (Sing 0), Unj, Inj1 x1.

Apply unknownprop_3fe7f97dcb00bcf31cf989081bd8403f8f0647acc7dd719f8a7da64cd4837dac with Inj0 x0, Sing 0, Inj1 x1 leaving 2 subgoals.

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

Apply unknownprop_63c308b92260dbfca8c9530846e6836ba3e6be221cc8e80fd61db913e01bdacf with x0, Inj1, x1.

The subproof is completed by applying H0.

The subproof is completed by applying unknownprop_19d5e1f06b8ff33ed1f0a1ec773eb4ad1cafb04cacdc9f1d5ac58ef21224c105 with x1.

■

Proofgold Proof