Let x0 of type (ι → ο) → ο be given.

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

Assume H0: a4b00.. x0 = a4b00.. x1.

Apply functional extensionality with x0, x1.

Let x2 of type ι → ο be given.

Apply prop_ext_2 with x0 x2, x1 x2 leaving 2 subgoals.

Assume H1: x0 x2.

Claim L2: a4b00.. x1 (407b5.. x2)

Apply H0 with λ x3 x4 : ((ι → ο) → ο) → ο . x3 (407b5.. x2).

Let x3 of type ο be given.

Assume H2: ∀ x4 : ι → ο . and (407b5.. x2 = 407b5.. x4) (x0 x4) ⟶ x3.

Apply H2 with x2.

Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with 407b5.. x2 = 407b5.. x2, x0 x2 leaving 2 subgoals.

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

Assume H3: x4 (407b5.. x2) (407b5.. x2).

The subproof is completed by applying H3.

The subproof is completed by applying H1.

Apply L2 with x1 x2.

Let x3 of type ι → ο be given.

Assume H3: (λ x4 : ι → ο . and (407b5.. x2 = 407b5.. x4) (x1 x4)) x3.

Apply andE with 407b5.. x2 = 407b5.. x3, x1 x3, x1 x2 leaving 2 subgoals.

The subproof is completed by applying H3.

Assume H4: 407b5.. x2 = 407b5.. x3.

Assume H5: x1 x3.

Apply unknownprop_f6212d6ba4366f14f16f0857e6566c26f7bd27125deb5e4c2748921fd5fa9530 with x2, x3, λ x4 x5 : ι → ο . x1 x5 leaving 2 subgoals.

The subproof is completed by applying H4.

The subproof is completed by applying H5.

Assume H1: x1 x2.

Claim L2: a4b00.. x0 (407b5.. x2)

Apply H0 with λ x3 x4 : ((ι → ο) → ο) → ο . x4 (407b5.. x2).

Let x3 of type ο be given.

Assume H2: ∀ x4 : ι → ο . and (407b5.. x2 = 407b5.. x4) (x1 x4) ⟶ x3.

Apply H2 with x2.

Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with 407b5.. x2 = 407b5.. x2, x1 x2 leaving 2 subgoals.

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

Assume H3: x4 (407b5.. x2) (407b5.. x2).

The subproof is completed by applying H3.

The subproof is completed by applying H1.

Apply L2 with x0 x2.

Let x3 of type ι → ο be given.

Assume H3: (λ x4 : ι → ο . and (407b5.. x2 = 407b5.. x4) (x0 x4)) x3.

Apply andE with 407b5.. x2 = 407b5.. x3, x0 x3, x0 x2 leaving 2 subgoals.

The subproof is completed by applying H3.

Assume H4: 407b5.. x2 = 407b5.. x3.

Assume H5: x0 x3.

Apply unknownprop_f6212d6ba4366f14f16f0857e6566c26f7bd27125deb5e4c2748921fd5fa9530 with x2, x3, λ x4 x5 : ι → ο . x0 x5 leaving 2 subgoals.

The subproof is completed by applying H4.

The subproof is completed by applying H5.

■

Proofgold Proof