Let x0 of type ι → ο be given.

Let x1 of type ι → ο be given.

Let x2 of type ι be given.

Let x3 of type ι be given.

Assume H0: x0 x2.

Assume H1: x1 x3.

Let x4 of type ο be given.

Assume H2: ∀ x5 . (∃ x6 . and (and (x0 x5) (x1 x6)) (cfc98.. x2 x3 = cfc98.. x5 x6)) ⟶ x4.

Apply H2 with x2.

Let x5 of type ο be given.

Assume H3: ∀ x6 . and (and (x0 x2) (x1 x6)) (cfc98.. x2 x3 = cfc98.. x2 x6) ⟶ x5.

Apply H3 with x3.

Apply and3I with x0 x2, x1 x3, cfc98.. x2 x3 = cfc98.. x2 x3 leaving 3 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

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

Assume H4: x6 (cfc98.. x2 x3) (cfc98.. x2 x3).

The subproof is completed by applying H4.

■

Proofgold Proof