Assume H0: ∀ x0 : ι → ι → ο . ∀ x1 : ι → ι → ι . ∀ x2 x3 : ι → ο . ∀ x4 : ι → ι . ∀ x5 x6 x7 . ∃ x8 . and (x8 = x7) (x4 (x1 (x1 (x4 (x1 (x1 (x1 (x1 (x1 x5 x7) (x4 (x4 (x1 (x1 x7 x5) x7)))) (x1 (x1 x5 x5) (x1 (x4 x5) (x1 x7 (x1 (x4 x5) x8))))) x8) x8)) x5) (x4 x5)) = x6).

Claim L1: ∃ x0 . and (x0 = 0) (0 = Power 0)

The subproof is completed by applying H0 with λ x0 x1 . False, λ x0 x1 . 0, λ x0 . False, λ x0 . False, λ x0 . 0, 0, Power 0, 0.

Claim L2: 0 = Power 0

Apply L1 with 0 = Power 0.

Let x0 of type ι be given.

Assume H2: and (x0 = 0) (0 = Power 0).

Apply unknownprop_896ccc9f209efa8a895211d65adb5a90348b419f100f6ab5e9762ce4d7fa9cc1 with x0 = 0, 0 = Power 0.

The subproof is completed by applying H2.

Apply FalseE.

Apply unknownprop_03947e47f83a9d5e72cb98dd3f209204911913d012cc97eaa0c7893a771d889d.

The subproof is completed by applying L2.

■

Proofgold Proof