Let x0 of type ι be given.

Let x1 of type ι → ι → ι be given.

Let x2 of type ι be given.

Let x3 of type ι → ι be given.

Let x4 of type ι → ι be given.

Assume H0: ∀ x5 . In x5 x2 ⟶ x3 x5 = x4 x5.

Apply unknownprop_b257b354d80b58d9a8444b167a21f47b4aabc910dc3698404491d5ef01e18cf3 with In (Union x2) x2, (λ x5 . λ x6 : ι → ι . If_i (In (Union x5) x5) (x1 (Union x5) (x6 (Union x5))) x0) x2 x3 = (λ x5 . λ x6 : ι → ι . If_i (In (Union x5) x5) (x1 (Union x5) (x6 (Union x5))) x0) x2 x4 leaving 2 subgoals.

Assume H1: In (Union x2) x2.

Apply H0 with Union x2, λ x5 x6 . If_i (In (Union x2) x2) (x1 (Union x2) x6) x0 = If_i (In (Union x2) x2) (x1 (Union x2) (x4 (Union x2))) x0 leaving 2 subgoals.

The subproof is completed by applying H1.

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

Assume H2: x5 (If_i (In (Union x2) x2) (x1 (Union x2) (x4 (Union x2))) x0) (If_i (In (Union x2) x2) (x1 (Union x2) (x4 (Union x2))) x0).

The subproof is completed by applying H2.

Assume H1: not (In (Union x2) x2).

Claim L2: If_i (In (Union x2) x2) (x1 (Union x2) (x3 (Union x2))) x0 = x0

Apply unknownprop_5a150bd86f4285de5d98c60b17d4452a655b4d88de0a02247259cdad6e6d992c with In (Union x2) x2, x1 (Union x2) (x3 (Union x2)), x0.

The subproof is completed by applying H1.

Claim L3: If_i (In (Union x2) x2) (x1 (Union x2) (x4 (Union x2))) x0 = x0

Apply unknownprop_5a150bd86f4285de5d98c60b17d4452a655b4d88de0a02247259cdad6e6d992c with In (Union x2) x2, x1 (Union x2) (x4 (Union x2)), x0.

The subproof is completed by applying H1.

Apply L3 with λ x5 x6 . If_i (In (Union x2) x2) (x1 (Union x2) (x3 (Union x2))) x0 = x6.

The subproof is completed by applying L2.

■

Proofgold Proof