Let x0 of type ι be given.

Let x1 of type ι be given.

Apply Subq_binintersection_eq with x0, x1, λ x2 x3 : ο . x3 ⟶ x1 = binunion x0 (setminus x1 x0).

Assume H0: binintersect x0 x1 = x0.

Apply unknownprop_d80a5cdd35aff682e6edc37d56782355ff9ceaa0a69a0eeabe526b6102deafb2 with x1, x0, λ x2 x3 . x3 = binunion x0 (setminus x1 x0).

Apply binunion_com with setminus x1 x0, binintersect x1 x0, λ x2 x3 . x3 = binunion x0 (setminus x1 x0).

set y2 to be binunion (binintersect x1 x0) (setminus x1 x0)

set y3 to be binunion x1 (setminus y2 x1)

Claim L1: ∀ x4 : ι → ο . x4 y3 ⟶ x4 y2

Let x4 of type ι → ο be given.

Assume H1: x4 (binunion y2 (setminus y3 y2)).

set y5 to be λ x5 . x4

Apply binintersect_com with y3, y2, λ x6 x7 . x7 = y2, λ x6 x7 . y5 (binunion x6 (setminus y3 y2)) (binunion x7 (setminus y3 y2)) leaving 2 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

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

Apply L1 with λ x5 . x4 x5 y3 ⟶ x4 y3 x5.

Assume H2: x4 y3 y3.

The subproof is completed by applying H2.

■

Proofgold Proof