Let x0 of type ι be given.

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

Assume H0: x1 4a7ef.. x0.

Assume H1: ∀ x2 . ba9d8.. x2 ⟶ ∀ x3 . aa8d2.. x2 x0 x3 ⟶ x1 x2 x3 ⟶ x1 (4ae4a.. x2) (prim3 x3).

Claim L2: ∀ x2 . ba9d8.. x2 ⟶ ∀ x3 . aa8d2.. x2 x0 x3 ⟶ (λ x4 x5 . and (aa8d2.. x4 x0 x5) (x1 x4 x5)) x2 x3

Let x2 of type ι be given.

Assume H2: ba9d8.. x2.

Let x3 of type ι be given.

Assume H3: aa8d2.. x2 x0 x3.

Apply H3 with λ x4 x5 . and (aa8d2.. x4 x0 x5) (x1 x4 x5) leaving 2 subgoals.

Apply andI with aa8d2.. 4a7ef.. x0 x0, x1 4a7ef.. x0 leaving 2 subgoals.

The subproof is completed by applying unknownprop_f8eb3f19a7c6d972011b74d047027c2ca36c9a4aeb442692e92508e3371c0d54 with x0.

The subproof is completed by applying H0.

Let x4 of type ι be given.

Assume H4: ba9d8.. x4.

Let x5 of type ι be given.

Assume H5: (λ x6 x7 . and (aa8d2.. x6 x0 x7) (x1 x6 x7)) x4 x5.

Apply H5 with (λ x6 x7 . and (aa8d2.. x6 x0 x7) (x1 x6 x7)) (4ae4a.. x4) (prim3 x5).

Assume H6: aa8d2.. x4 x0 x5.

Assume H7: x1 x4 x5.

Apply andI with aa8d2.. (4ae4a.. x4) x0 (prim3 x5), x1 (4ae4a.. x4) (prim3 x5) leaving 2 subgoals.

Apply unknownprop_a538fde2cb1c64ff6668f36b93c17f835ee2f07e6e0a0f90d30947fd8d72de1a with x0, x4, x5 leaving 2 subgoals.

The subproof is completed by applying H4.

The subproof is completed by applying H6.

Apply H1 with x4, x5 leaving 3 subgoals.

The subproof is completed by applying H4.

The subproof is completed by applying H6.

The subproof is completed by applying H7.

Let x2 of type ι be given.

Let x3 of type ι be given.

Assume H3: ba9d8.. x2.

Assume H4: aa8d2.. x2 x0 x3.

Apply andER with aa8d2.. x2 x0 x3, x1 x2 x3.

Apply L2 with x2, x3 leaving 2 subgoals.

The subproof is completed by applying H3.

The subproof is completed by applying H4.

■

Proofgold Proof