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

Claim L1: and (∀ x0 . 0 = x0 ⟶ and False (0 = 0 ⟶ and (∀ x1 . Power 0 = 0) (∃ x1 . False)) ⟶ ∃ x1 . 0 = 0) (not False) ⟶ 0 = Power 0

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

Claim L2: ∀ x0 . 0 = x0 ⟶ and False (0 = 0 ⟶ and (∀ x1 . Power 0 = 0) (∃ x1 . False)) ⟶ ∃ x1 . 0 = 0

Let x0 of type ι be given.

Assume H2: 0 = x0.

Assume H3: and False (0 = 0 ⟶ and (∀ x1 . Power 0 = 0) (∃ x1 . False)).

Apply unknownprop_8bd7560a9991903264b52a55534d2167a6f1ceb54602573e16d8e12432ce96be with λ x1 . 0 = 0, 0.

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

Assume H4: x1 0 0.

The subproof is completed by applying H4.

Claim L3: not False

Apply unknownprop_e284d5f5a7c3a1c03631041619c4ddee06de72330506f5f6d9d6b18df929e48c with False.

Assume H3: False.

The subproof is completed by applying H3.

Claim L4: and (∀ x0 . 0 = x0 ⟶ and False (0 = 0 ⟶ and (∀ x1 . Power 0 = 0) (∃ x1 . False)) ⟶ ∃ x1 . 0 = 0) (not False)

Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with ∀ x0 . 0 = x0 ⟶ and False (0 = 0 ⟶ and (∀ x1 . Power 0 = 0) (∃ x1 . False)) ⟶ ∃ x1 . 0 = 0, not False leaving 2 subgoals.

The subproof is completed by applying L2.

The subproof is completed by applying L3.

Claim L5: 0 = Power 0

Apply L1.

The subproof is completed by applying L4.

Apply FalseE.

Apply unknownprop_03947e47f83a9d5e72cb98dd3f209204911913d012cc97eaa0c7893a771d889d.

The subproof is completed by applying L5.

■

Proofgold Proof