Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Theorem 2435c.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ο . ∀ x2 : ι → ι . ∀ x3 : ι → ι → ι → ι . ∀ x4 x5 : ι → ι → ι . ∀ x6 . ∀ x7 : ι → ι → ι . ∀ x8 x9 x10 x11 . ∀ x12 x13 : ι → ι . ∀ x14 : ι → ι → ι → ι . ∀ x15 : ι → ι → ι → ο . ∀ x16 x17 : ι → ι . ∀ x18 : ι → ι → ο . ∀ x19 : ι → ι → ι → ι . ∀ x20 : ι → ι → ι . ∀ x21 : ι → ι → ι → ι . ∀ x22 : ι → ι . ∀ x23 : ι → ο . (∀ x24 x25 x26 x27 . x23 x27 ⟶ x15 x24 (x17 x27) (x16 x27) ⟶ x15 x26 (x17 x27) (x16 x27) ⟶ x15 x25 (x17 x27) (x16 x27) ⟶ (x18 (x19 x27 (x19 x27 x24 x26) (x19 x27 (x20 x27 (x21 x27 x26 x25)) (x20 x27 (x21 x27 x24 x25)))) (x22 x27) ⟶ False) ⟶ False) ⟶ (∀ x24 x25 x26 . (x0 x26 ⟶ False) ⟶ (x0 x24 ⟶ False) ⟶ x1 x24 (x2 x26) ⟶ x1 x25 x24 ⟶ (x15 x25 x26 x24 ⟶ False) ⟶ False) ⟶ (∀ x24 x25 x26 . (x0 x26 ⟶ False) ⟶ (x0 x24 ⟶ False) ⟶ x1 x24 (x2 x26) ⟶ x15 x25 x26 x24 ⟶ (x1 x25 x24 ⟶ False) ⟶ False) ⟶ (∀ x24 x25 x26 . x23 x26 ⟶ x1 x24 (x16 x26) ⟶ x1 x25 (x16 x26) ⟶ (x19 x26 x24 x25 = x3 x26 x24 x25 ⟶ False) ⟶ False) ⟶ (∀ x24 x25 x26 . x23 x26 ⟶ x1 x24 (x16 x26) ⟶ x1 x25 (x16 x26) ⟶ (x21 x26 x24 x25 = x14 x26 x24 x25 ⟶ False) ⟶ False) ⟶ (∀ x24 x25 . x23 x25 ⟶ x1 x24 (x16 x25) ⟶ (x20 x25 x24 = x4 x25 x24 ⟶ False) ⟶ False) ⟶ (∀ x24 . x23 x24 ⟶ x0 (x16 x24) ⟶ False) ⟶ (∀ x24 x25 . (x0 x25 ⟶ False) ⟶ (x0 x24 ⟶ False) ⟶ x1 x24 (x2 x25) ⟶ (x15 (x5 x24 x25) x25 x24 ⟶ False) ⟶ False) ⟶ (∀ x24 . (x1 (x13 x24) x24 ⟶ False) ⟶ False) ⟶ ((x23 x6 ⟶ False) ⟶ False) ⟶ (∀ x24 x25 x26 . (x0 x26 ⟶ False) ⟶ (x0 x24 ⟶ False) ⟶ x1 x24 (x2 x26) ⟶ x15 x25 x26 x24 ⟶ (x1 x25 x26 ⟶ False) ⟶ False) ⟶ (∀ x24 . x23 x24 ⟶ x0 (x17 x24) ⟶ False) ⟶ (∀ x24 x25 x26 . x23 x26 ⟶ x1 x24 (x16 x26) ⟶ x1 x25 (x16 x26) ⟶ (x15 (x19 x26 x24 x25) (x17 x26) (x16 x26) ⟶ False) ⟶ False) ⟶ (∀ x24 x25 x26 . x23 x26 ⟶ x1 x24 (x16 x26) ⟶ x1 x25 (x16 x26) ⟶ (x15 (x21 x26 x24 x25) (x17 x26) (x16 x26) ⟶ False) ⟶ False) ⟶ (∀ x24 x25 . x23 x25 ⟶ x1 x24 (x16 x25) ⟶ (x15 (x20 x25 x24) (x17 x25) (x16 x25) ⟶ False) ⟶ False) ⟶ (∀ x24 . x23 x24 ⟶ (x1 (x22 x24) (x2 (x16 x24)) ⟶ False) ⟶ False) ⟶ (∀ x24 . x23 x24 ⟶ (x1 (x16 x24) (x2 (x17 x24)) ⟶ False) ⟶ False) ⟶ (∀ x24 x25 x26 . x23 x26 ⟶ x1 x24 (x17 x26) ⟶ x1 x25 (x17 x26) ⟶ (x1 (x3 x26 x24 x25) (x17 x26) ⟶ False) ⟶ False) ⟶ (∀ x24 . (x1 (x12 x24) (x2 x24) ⟶ False) ⟶ False) ⟶ (∀ x24 x25 . x23 x25 ⟶ x1 x24 (x2 (x16 x25)) ⟶ (x1 (x7 x25 x24) (x2 (x16 x25)) ⟶ False) ⟶ False) ⟶ (∀ x24 x25 x26 . x23 x26 ⟶ x1 x24 (x17 x26) ⟶ x1 x25 (x17 x26) ⟶ (x1 (x14 x26 x24 x25) (x17 x26) ⟶ False) ⟶ False) ⟶ (∀ x24 x25 . x23 x25 ⟶ x1 x24 (x17 x25) ⟶ (x1 (x4 x25 x24) (x17 x25) ⟶ False) ⟶ False) ⟶ (∀ x24 . x23 x24 ⟶ (x22 x24 = x7 x24 (x12 (x16 x24)) ⟶ False) ⟶ False) ⟶ (∀ x24 x25 x26 . x23 x26 ⟶ x1 x24 (x17 x26) ⟶ x1 x25 (x17 x26) ⟶ (x3 x26 x24 x25 = x4 x26 (x14 x26 x24 (x4 x26 x25)) ⟶ False) ⟶ False) ⟶ (∀ x24 x25 . x18 x24 x25 ⟶ x18 x25 x24 ⟶ False) ⟶ (x18 (x19 x8 (x19 x8 x10 x11) (x19 x8 (x19 x8 x11 x9) (x19 x8 x10 x9))) (x22 x8) ⟶ False) ⟶ ((x15 x9 (x17 x8) (x16 x8) ⟶ False) ⟶ False) ⟶ ((x15 x11 (x17 x8) (x16 x8) ⟶ False) ⟶ False) ⟶ ((x15 x10 (x17 x8) (x16 x8) ⟶ False) ⟶ False) ⟶ ((x23 x8 ⟶ False) ⟶ False) ⟶ False (proof)

Proofgold Asset