Let x0 of type ι → ο be given.

Let x1 of type ι → ο be given.

Let x2 of type ι be given.

Assume H0: c0709.. x0 x1 x2.

Let x3 of type ι → ο be given.

Assume H1: ∀ x4 . x0 x4 ⟶ x3 (0b8ef.. x4).

Assume H2: ∀ x4 . x1 x4 ⟶ x3 (6c5f4.. x4).

Apply H0 with x3 x2 leaving 2 subgoals.

Assume H3: ∃ x4 . and (x0 x4) (x2 = 0b8ef.. x4).

Apply H3 with x3 x2.

Let x4 of type ι be given.

Assume H4: (λ x5 . and (x0 x5) (x2 = 0b8ef.. x5)) x4.

Apply H4 with x3 x2.

Assume H5: x0 x4.

Assume H6: x2 = 0b8ef.. x4.

Apply H6 with λ x5 x6 . x3 x6.

Apply H1 with x4.

The subproof is completed by applying H5.

Assume H3: ∃ x4 . and (x1 x4) (x2 = 6c5f4.. x4).

Apply H3 with x3 x2.

Let x4 of type ι be given.

Assume H4: (λ x5 . and (x1 x5) (x2 = 6c5f4.. x5)) x4.

Apply H4 with x3 x2.

Assume H5: x1 x4.

Assume H6: x2 = 6c5f4.. x4.

Apply H6 with λ x5 x6 . x3 x6.

Apply H2 with x4.

The subproof is completed by applying H5.

■

Proofgold Proof