Apply unknownprop_72dc8a048701bf51fd7b8ba6b7bf88eb6b499e1dce5a6cc41194ad4cd8a8616a with λ x0 . λ x1 : ι → ο . ∀ x2 . ∀ x3 : ι → ο . 858ff.. x2 x3 ⟶ x0 = x2 ⟶ x1 = x3 leaving 3 subgoals.

Apply unknownprop_72dc8a048701bf51fd7b8ba6b7bf88eb6b499e1dce5a6cc41194ad4cd8a8616a with λ x0 . λ x1 : ι → ο . 5e331.. = x0 ⟶ 07017.. = x1 leaving 3 subgoals.

Assume H0: 5e331.. = 5e331...

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

Assume H1: x0 07017.. 07017...

The subproof is completed by applying H1.

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: 858ff.. x0 x2.

Assume H1: 5e331.. = x0 ⟶ 07017.. = x2.

Assume H2: 858ff.. x1 x3.

Assume H3: 5e331.. = x1 ⟶ 07017.. = x3.

Assume H4: 5e331.. = a3eb9.. x0 x1.

Apply FalseE with 07017.. = c0709.. x2 x3.

Apply unknownprop_112da44b75efcdc251767c8f8619fc43c6b883afd5ac71e5854bf36b62571f0c with x0, x1.

The subproof is completed by applying H4.

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: 858ff.. x0 x2.

Assume H1: 5e331.. = x0 ⟶ 07017.. = x2.

Assume H2: 858ff.. x1 x3.

Assume H3: 5e331.. = x1 ⟶ 07017.. = x3.

Assume H4: 5e331.. = bf68c.. x0 x1.

Apply FalseE with 07017.. = 6e020.. x2 x3.

Apply unknownprop_951e3ef812229b5945a39a7fa79f4fd40c15277c7d728e18721eb777036d91be with x0, x1.

The subproof is completed by applying H4.

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: 858ff.. x0 x2.

Assume H1: ∀ x4 . ∀ x5 : ι → ο . 858ff.. x4 x5 ⟶ x0 = x4 ⟶ x2 = x5.

Assume H2: 858ff.. x1 x3.

Assume H3: ∀ x4 . ∀ x5 : ι → ο . 858ff.. x4 x5 ⟶ x1 = x4 ⟶ x3 = x5.

Apply unknownprop_72dc8a048701bf51fd7b8ba6b7bf88eb6b499e1dce5a6cc41194ad4cd8a8616a with λ x4 . λ x5 : ι → ο . a3eb9.. x0 x1 = x4 ⟶ c0709.. x2 x3 = x5 leaving 3 subgoals.

Assume H4: a3eb9.. x0 x1 = 5e331...

Apply FalseE with c0709.. x2 x3 = 07017...

Apply unknownprop_112da44b75efcdc251767c8f8619fc43c6b883afd5ac71e5854bf36b62571f0c with x0, x1.

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

The subproof is completed by applying H4 with λ x5 x6 . x4 x6 x5.

Let x4 of type ι be given.

Let x5 of type ι be given.

Let x6 of type ι → ο be given.

Let x7 of type ι → ο be given.

Assume H4: 858ff.. x4 x6.

Assume H5: a3eb9.. x0 x1 = x4 ⟶ c0709.. x2 x3 = x6.

Assume H6: 858ff.. x5 x7.

Assume H7: a3eb9.. x0 x1 = x5 ⟶ c0709.. x2 x3 = x7.

Assume H8: a3eb9.. x0 x1 = a3eb9.. x4 x5.

Apply unknownprop_1f81fbea8647063ecd1729d03bf27a5327e4a018cc4ad3e99f64b38027811c93 with x0, x1, x4, x5, c0709.. x2 x3 = c0709.. x6 x7 leaving 2 subgoals.

The subproof is completed by applying H8.

Assume H9: x0 = x4.

Assume H10: x1 = x5.

Claim L11: x2 = x6

Apply H1 with x4, x6 leaving 2 subgoals.

The subproof is completed by applying H4.

The subproof is completed by applying H9.

Claim L12: x3 = x7

Apply H3 with x5, x7 leaving 2 subgoals.

The subproof is completed by applying H6.

The subproof is completed by applying H10.

Apply L11 with λ x8 x9 : ι → ο . c0709.. x9 x3 = c0709.. x6 x7.

Apply L12 with λ x8 x9 : ι → ο . c0709.. x6 x9 = c0709.. x6 x7.

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

Assume H13: x8 (c0709.. x6 x7) (c0709.. x6 x7).

The subproof is completed by applying H13.

Let x4 of type ι be given.

...

■

Proofgold Proof