Proofgold Proof

pf

Let x0 of type ι be given.

Assume H0: x0 ∈ u6.

Let x1 of type ο be given.

Apply cases_6 with x0, λ x2 . (∀ x3 : ι → ι → ι → ι → ι → ι → ι . Church6_p x3 ⟶ x2 = Church6_to_u6 x3 ⟶ x1) ⟶ x1 leaving 7 subgoals.

The subproof is completed by applying H0.

Assume H1: ∀ x2 : ι → ι → ι → ι → ι → ι → ι . Church6_p x2 ⟶ 0 = Church6_to_u6 x2 ⟶ x1.

Apply H1 with λ x2 x3 x4 x5 x6 x7 . x2 leaving 2 subgoals.

The subproof is completed by applying unknownprop_331adedb7edd49a25927b93fceb0218da7c5b54994dbd262dd5d161f43c67d7a.

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

Assume H2: x2 0 (Church6_to_u6 (λ x3 x4 x5 x6 x7 x8 . x3)).

The subproof is completed by applying H2.

Assume H1: ∀ x2 : ι → ι → ι → ι → ι → ι → ι . Church6_p x2 ⟶ u1 = Church6_to_u6 x2 ⟶ x1.

Apply H1 with λ x2 x3 x4 x5 x6 x7 . x3 leaving 2 subgoals.

The subproof is completed by applying unknownprop_043e4b78a0654a6683c9234d3bf7766badd8de7fbbde08ad6810ddd8a4f5acef.

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

Assume H2: x2 u1 (Church6_to_u6 (λ x3 x4 x5 x6 x7 x8 . x4)).

The subproof is completed by applying H2.

Assume H1: ∀ x2 : ι → ι → ι → ι → ι → ι → ι . Church6_p x2 ⟶ u2 = Church6_to_u6 x2 ⟶ x1.

Apply H1 with λ x2 x3 x4 x5 x6 x7 . x4 leaving 2 subgoals.

The subproof is completed by applying unknownprop_616c991f45f4fe9d3efb0220d6bfc2b3a9576d02c827cfd1aa156159e180bc78.

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

Assume H2: x2 u2 (Church6_to_u6 (λ x3 x4 x5 x6 x7 x8 . x5)).

The subproof is completed by applying H2.

Assume H1: ∀ x2 : ι → ι → ι → ι → ι → ι → ι . Church6_p x2 ⟶ u3 = Church6_to_u6 x2 ⟶ x1.

Apply H1 with λ x2 x3 x4 x5 x6 x7 . x5 leaving 2 subgoals.

The subproof is completed by applying unknownprop_829cc6bcf19535104e1ef14d3c37a121ee539b24777eaff2cd61aead27db443c.

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

Assume H2: x2 u3 (Church6_to_u6 (λ x3 x4 x5 x6 x7 x8 . x6)).

The subproof is completed by applying H2.

Assume H1: ∀ x2 : ι → ι → ι → ι → ι → ι → ι . Church6_p x2 ⟶ u4 = Church6_to_u6 x2 ⟶ x1.

Apply H1 with λ x2 x3 x4 x5 x6 x7 . x6 leaving 2 subgoals.

The subproof is completed by applying unknownprop_c2058c433a08cbd0a9de8592bbafc20a46c3ba8f1b81c7ac182023aff037fe72.

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

Assume H2: x2 u4 (Church6_to_u6 (λ x3 x4 x5 x6 x7 x8 . x7)).

The subproof is completed by applying H2.

Assume H1: ∀ x2 : ι → ι → ι → ι → ι → ι → ι . Church6_p x2 ⟶ u5 = Church6_to_u6 x2 ⟶ x1.

Apply H1 with λ x2 x3 x4 x5 x6 x7 . x7 leaving 2 subgoals.

The subproof is completed by applying unknownprop_4d8598615c468fd2c2438610c865b021fd567a1a56272aa5746a1a4686cd4fd4.

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

Assume H2: x2 u5 (Church6_to_u6 (λ x3 x4 x5 x6 x7 x8 . x8)).

The subproof is completed by applying H2.

■