Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Theorem 3e41f.. : ∀ 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 : ι → ι → ι → ι . ∀ x28 x29 : ι → ο . (∀ x30 x31 x32 . (x29 x32 ⟶ False) ⟶ x22 x32 ⟶ x28 x32 ⟶ x24 x30 (x23 x32) ⟶ x24 x31 (x23 x32) ⟶ (x26 x32 (x25 x32 x30 x31) = x27 x32 (x26 x32 x30) (x26 x32 x31) ⟶ False) ⟶ False) ⟶ (∀ x30 x31 x32 . (x29 x32 ⟶ False) ⟶ x22 x32 ⟶ x28 x32 ⟶ x24 x30 (x23 x32) ⟶ x24 x31 (x23 x32) ⟶ (x26 x32 (x27 x32 x30 x31) = x25 x32 (x26 x32 x30) (x26 x32 x31) ⟶ False) ⟶ False) ⟶ (∀ x30 x31 x32 x33 . x21 x33 ⟶ x18 x33 ⟶ x28 x33 ⟶ x24 x30 (x23 x33) ⟶ x24 x32 (x23 x33) ⟶ x24 x31 (x23 x33) ⟶ x20 x33 ⟶ (x19 x33 (x19 x33 x30 x32) x31 = x19 x33 x30 (x19 x33 x32 x31) ⟶ False) ⟶ False) ⟶ (∀ x30 x31 x32 . x21 x32 ⟶ x1 x32 ⟶ x28 x32 ⟶ x24 x30 (x23 x32) ⟶ x24 x31 (x23 x32) ⟶ (x27 x32 x30 x31 = x0 x32 x30 x31 ⟶ False) ⟶ False) ⟶ (∀ x30 x31 x32 . x21 x32 ⟶ x18 x32 ⟶ x28 x32 ⟶ x24 x30 (x23 x32) ⟶ x24 x31 (x23 x32) ⟶ (x25 x32 x30 x31 = x19 x32 x30 x31 ⟶ False) ⟶ False) ⟶ (∀ x30 . (x24 (x2 x30) x30 ⟶ False) ⟶ False) ⟶ ((x17 x16 ⟶ False) ⟶ False) ⟶ ((x28 x3 ⟶ False) ⟶ False) ⟶ (∀ x30 . x28 x30 ⟶ (x17 x30 ⟶ False) ⟶ False) ⟶ (∀ x30 x31 . (x29 x31 ⟶ False) ⟶ x28 x31 ⟶ x24 x30 (x23 x31) ⟶ (x24 (x26 x31 x30) (x23 x31) ⟶ False) ⟶ False) ⟶ (∀ x30 x31 x32 . (x29 x32 ⟶ False) ⟶ x28 x32 ⟶ x24 x31 (x23 x32) ⟶ x24 x30 (x23 x32) ⟶ (x24 (x15 x32 x31 x30) (x23 x32) ⟶ False) ⟶ False) ⟶ (∀ x30 x31 x32 . x21 x32 ⟶ x1 x32 ⟶ x28 x32 ⟶ x24 x30 (x23 x32) ⟶ x24 x31 (x23 x32) ⟶ (x24 (x27 x32 x30 x31) (x23 x32) ⟶ False) ⟶ False) ⟶ (∀ x30 x31 x32 . x21 x32 ⟶ x18 x32 ⟶ x28 x32 ⟶ x24 x30 (x23 x32) ⟶ x24 x31 (x23 x32) ⟶ (x24 (x25 x32 x30 x31) (x23 x32) ⟶ False) ⟶ False) ⟶ (∀ x30 x31 x32 . x28 x32 ⟶ x24 x30 (x23 x32) ⟶ x24 x31 (x23 x32) ⟶ (x24 (x19 x32 x30 x31) (x23 x32) ⟶ False) ⟶ False) ⟶ (∀ x30 x31 x32 . x28 x32 ⟶ x24 x30 (x23 x32) ⟶ x24 x31 (x23 x32) ⟶ (x24 (x0 x32 x30 x31) (x23 x32) ⟶ False) ⟶ False) ⟶ (∀ x30 x31 x32 . (x29 x32 ⟶ False) ⟶ x28 x32 ⟶ x24 x31 (x23 x32) ⟶ x24 x30 (x23 x32) ⟶ (x15 x32 x31 x30 = x19 x32 x31 (x26 x32 x30) ⟶ False) ⟶ False) ⟶ (∀ x30 x31 x32 . x21 x32 ⟶ x1 x32 ⟶ x28 x32 ⟶ x24 x30 (x23 x32) ⟶ x24 x31 (x23 x32) ⟶ (x27 x32 x30 x31 = x27 x32 x31 x30 ⟶ False) ⟶ False) ⟶ (∀ x30 x31 x32 . x21 x32 ⟶ x18 x32 ⟶ x28 x32 ⟶ x24 x30 (x23 x32) ⟶ x24 x31 (x23 x32) ⟶ (x25 x32 x30 x31 = x25 x32 x31 x30 ⟶ False) ⟶ False) ⟶ (∀ x30 . x28 x30 ⟶ (x29 x30 ⟶ False) ⟶ x14 x30 ⟶ x20 x30 ⟶ x21 x30 ⟶ x1 x30 ⟶ x18 x30 ⟶ x11 x30 ⟶ x13 x30 ⟶ x12 x30 ⟶ (x22 x30 ⟶ False) ⟶ False) ⟶ (∀ x30 . x28 x30 ⟶ (x29 x30 ⟶ False) ⟶ x14 x30 ⟶ x20 x30 ⟶ x21 x30 ⟶ x1 x30 ⟶ x18 x30 ⟶ x11 x30 ⟶ x13 x30 ⟶ x12 x30 ⟶ x29 x30 ⟶ False) ⟶ (∀ x30 . x28 x30 ⟶ (x29 x30 ⟶ False) ⟶ x22 x30 ⟶ (x12 x30 ⟶ False) ⟶ False) ⟶ (∀ x30 . x28 x30 ⟶ (x29 x30 ⟶ False) ⟶ x22 x30 ⟶ (x13 x30 ⟶ False) ⟶ False) ⟶ (∀ x30 . x28 x30 ⟶ (x29 x30 ⟶ False) ⟶ x22 x30 ⟶ (x11 x30 ⟶ False) ⟶ False) ⟶ (∀ x30 . x28 x30 ⟶ (x29 x30 ⟶ False) ⟶ x22 x30 ⟶ (x18 x30 ⟶ False) ⟶ False) ⟶ (∀ x30 . x28 x30 ⟶ (x29 x30 ⟶ False) ⟶ x22 x30 ⟶ (x1 x30 ⟶ False) ⟶ False) ⟶ (∀ x30 . x28 x30 ⟶ (x29 x30 ⟶ False) ⟶ x22 x30 ⟶ (x21 x30 ⟶ False) ⟶ False) ⟶ (∀ x30 . x28 x30 ⟶ (x29 x30 ⟶ False) ⟶ x22 x30 ⟶ (x20 x30 ⟶ False) ⟶ False) ⟶ (∀ x30 . x28 x30 ⟶ (x29 x30 ⟶ False) ⟶ x22 x30 ⟶ (x14 x30 ⟶ False) ⟶ False) ⟶ (∀ x30 . x28 x30 ⟶ (x29 x30 ⟶ False) ⟶ x22 x30 ⟶ x29 x30 ⟶ False) ⟶ (∀ x30 . x28 x30 ⟶ (x29 x30 ⟶ False) ⟶ x5 x30 ⟶ (x4 x30 ⟶ False) ⟶ False) ⟶ (∀ x30 . x28 x30 ⟶ (x29 x30 ⟶ False) ⟶ x5 x30 ⟶ x29 x30 ⟶ False) ⟶ (∀ x30 . x28 x30 ⟶ (x29 x30 ⟶ False) ⟶ x5 x30 ⟶ (x13 x30 ⟶ False) ⟶ False) ⟶ (∀ x30 . x28 x30 ⟶ (x29 x30 ⟶ False) ⟶ x5 x30 ⟶ x29 x30 ⟶ False) ⟶ (∀ x30 . x28 x30 ⟶ x6 x30 ⟶ x4 x30 ⟶ (x11 x30 ⟶ False) ⟶ False) ⟶ (∀ x30 . x28 x30 ⟶ (x29 x30 ⟶ False) ⟶ x5 x30 ⟶ (x18 x30 ⟶ False) ⟶ False) ⟶ (∀ x30 . x28 x30 ⟶ (x29 x30 ⟶ False) ⟶ x5 x30 ⟶ (x1 x30 ⟶ False) ⟶ False) ⟶ (∀ x30 . x28 x30 ⟶ (x29 x30 ⟶ False) ⟶ x5 x30 ⟶ (x21 x30 ⟶ False) ⟶ False) ⟶ (∀ x30 . x28 x30 ⟶ (x29 x30 ⟶ False) ⟶ x5 x30 ⟶ (x20 x30 ⟶ False) ⟶ False) ⟶ (∀ x30 . x28 x30 ⟶ (x29 x30 ⟶ False) ⟶ x5 x30 ⟶ (x14 x30 ⟶ False) ⟶ False) ⟶ (∀ x30 . x28 x30 ⟶ (x29 x30 ⟶ False) ⟶ x5 x30 ⟶ x29 x30 ⟶ False) ⟶ (∀ x30 . x28 x30 ⟶ x11 x30 ⟶ (x4 x30 ⟶ False) ⟶ False) ⟶ (∀ x30 . x28 x30 ⟶ x11 x30 ⟶ (x6 x30 ⟶ False) ⟶ False) ⟶ (∀ x30 . x28 x30 ⟶ x18 x30 ⟶ x29 x30 ⟶ False) ⟶ (∀ x30 . x28 x30 ⟶ x1 x30 ⟶ x29 x30 ⟶ False) ⟶ (∀ x30 . x28 x30 ⟶ (x29 x30 ⟶ False) ⟶ x22 x30 ⟶ (x5 x30 ⟶ False) ⟶ False) ⟶ (∀ x30 . x28 x30 ⟶ (x29 x30 ⟶ False) ⟶ x22 x30 ⟶ x29 x30 ⟶ False) ⟶ (x15 x10 (x15 x10 x8 x9) x7 = x15 x10 x8 (x27 x10 x9 x7) ⟶ False) ⟶ ((x24 x7 (x23 x10) ⟶ False) ⟶ False) ⟶ ((x24 x9 (x23 x10) ⟶ False) ⟶ False) ⟶ ((x24 x8 (x23 x10) ⟶ False) ⟶ False) ⟶ ((x28 x10 ⟶ False) ⟶ False) ⟶ ((x22 x10 ⟶ False) ⟶ False) ⟶ (x29 x10 ⟶ False) ⟶ False (proof)

Proofgold Asset