Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Theorem 2b798.. : ∀ 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 . ∀ x33 : ι → ο . ∀ x34 x35 x36 . ∀ x37 : ι → ο . ∀ x38 : ι → ι → ι . ∀ x39 : ι → ι → ο . ∀ x40 : ι → ι → ι . ∀ x41 . (∀ x42 x43 . x43 = x41 ⟶ (x40 x42 x43 = x41 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 . x43 = x41 ⟶ (x40 x43 x42 = x41 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 . x40 x42 x43 = x41 ⟶ (x42 = x41 ⟶ False) ⟶ (x43 = x41 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 . x0 x43 ⟶ (x43 = x42 ⟶ False) ⟶ x0 x42 ⟶ False) ⟶ (∀ x42 x43 x44 x45 . x39 x44 x45 ⟶ x39 x43 x42 ⟶ (x39 (x38 x44 x43) (x40 x45 x42) ⟶ False) ⟶ False) ⟶ (∀ x42 x43 x44 x45 . x39 (x38 x43 x45) (x40 x42 x44) ⟶ (x39 x45 x44 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 x44 x45 . x39 (x38 x45 x43) (x40 x44 x42) ⟶ (x39 x45 x44 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 . x39 x42 x43 ⟶ x0 x43 ⟶ False) ⟶ (∀ x42 . x0 x42 ⟶ (x42 = x41 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 . x1 x42 x43 ⟶ (x0 x43 ⟶ False) ⟶ (x39 x42 x43 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 . x39 x43 x42 ⟶ (x1 x43 x42 ⟶ False) ⟶ False) ⟶ ((x2 x3 ⟶ False) ⟶ False) ⟶ (x0 x3 ⟶ False) ⟶ (x4 x5 ⟶ False) ⟶ ((x37 x5 ⟶ False) ⟶ False) ⟶ ((x6 x5 ⟶ False) ⟶ False) ⟶ ((x37 x36 ⟶ False) ⟶ False) ⟶ ((x7 x36 ⟶ False) ⟶ False) ⟶ ((x6 x36 ⟶ False) ⟶ False) ⟶ (x0 x36 ⟶ False) ⟶ ((x37 x35 ⟶ False) ⟶ False) ⟶ ((x7 x35 ⟶ False) ⟶ False) ⟶ ((x6 x35 ⟶ False) ⟶ False) ⟶ (x0 x8 ⟶ False) ⟶ ((x7 x34 ⟶ False) ⟶ False) ⟶ ((x6 x34 ⟶ False) ⟶ False) ⟶ ((x33 x32 ⟶ False) ⟶ False) ⟶ ((x37 x32 ⟶ False) ⟶ False) ⟶ ((x6 x32 ⟶ False) ⟶ False) ⟶ ((x9 x10 ⟶ False) ⟶ False) ⟶ ((x0 x31 ⟶ False) ⟶ False) ⟶ ((x6 x11 ⟶ False) ⟶ False) ⟶ (x0 x11 ⟶ False) ⟶ ((x37 x12 ⟶ False) ⟶ False) ⟶ ((x6 x12 ⟶ False) ⟶ False) ⟶ (∀ x42 . (x0 x42 ⟶ False) ⟶ x6 x42 ⟶ x0 (x13 x42) ⟶ False) ⟶ (∀ x42 . (x0 x42 ⟶ False) ⟶ x6 x42 ⟶ x0 (x30 x42) ⟶ False) ⟶ (∀ x42 x43 x44 x45 . (x6 (x14 (x38 x43 x42) (x38 x45 x44)) ⟶ False) ⟶ False) ⟶ (∀ x42 x43 . (x6 (x40 x42 x43) ⟶ False) ⟶ False) ⟶ (∀ x42 . x0 x42 ⟶ (x0 (x13 x42) ⟶ False) ⟶ False) ⟶ (∀ x42 x43 . (x6 (x29 (x38 x43 x42)) ⟶ False) ⟶ False) ⟶ (∀ x42 . x0 x42 ⟶ (x0 (x30 x42) ⟶ False) ⟶ False) ⟶ (∀ x42 x43 . x0 (x14 x42 x43) ⟶ False) ⟶ (∀ x42 . x0 (x29 x42) ⟶ False) ⟶ (∀ x42 . x28 x42 ⟶ x6 x42 ⟶ (x28 (x13 x42) ⟶ False) ⟶ False) ⟶ (∀ x42 . x28 x42 ⟶ x6 x42 ⟶ (x28 (x30 x42) ⟶ False) ⟶ False) ⟶ (∀ x42 x43 . (x9 (x38 x42 x43) ⟶ False) ⟶ False) ⟶ ((x0 x41 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 . (x37 (x29 (x38 x43 x42)) ⟶ False) ⟶ False) ⟶ (∀ x42 . (x28 x42 ⟶ False) ⟶ x6 x42 ⟶ x37 x42 ⟶ x28 (x30 x42) ⟶ False) ⟶ (∀ x42 x43 . x6 x43 ⟶ x37 x43 ⟶ x6 x42 ⟶ x37 x42 ⟶ (x2 (x14 x43 x42) ⟶ False) ⟶ False) ⟶ (∀ x42 . x6 x42 ⟶ x37 x42 ⟶ (x2 (x29 x42) ⟶ False) ⟶ False) ⟶ (∀ x42 . x6 x42 ⟶ x37 x42 ⟶ (x4 x42 ⟶ False) ⟶ x28 (x13 x42) ⟶ False) ⟶ (∀ x42 . x6 x42 ⟶ x37 x42 ⟶ x4 x42 ⟶ (x28 (x13 x42) ⟶ False) ⟶ False) ⟶ (∀ x42 . x0 x42 ⟶ (x0 (x13 x42) ⟶ False) ⟶ False) ⟶ (∀ x42 x43 . (x0 x43 ⟶ False) ⟶ (x0 x42 ⟶ False) ⟶ x0 (x40 x43 x42) ⟶ False) ⟶ (∀ x42 . x0 x42 ⟶ (x0 (x30 x42) ⟶ False) ⟶ False) ⟶ (∀ x42 . x6 x42 ⟶ x7 x42 ⟶ x37 x42 ⟶ (x15 (x13 x42) ⟶ False) ⟶ False) ⟶ (∀ x42 . (x1 (x27 x42) x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . (x1 (x16 x42) x42 ⟶ False) ⟶ False) ⟶ ((x0 x26 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 . (x38 x43 x42 = x14 (x14 x43 x42) (x29 x43) ⟶ False) ⟶ False) ⟶ ((x41 = x26 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 . (x39 (x38 (x18 x43 x42) (x17 x43 x42)) x42 ⟶ False) ⟶ (x39 (x17 x43 x42) x43 ⟶ False) ⟶ (x43 = x13 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 x44 . x39 (x17 x44 x43) x44 ⟶ x39 (x38 x42 (x17 x44 x43)) x43 ⟶ (x44 = x13 x43 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 x44 x45 . x44 = x13 x45 ⟶ x39 (x38 x43 x42) x45 ⟶ (x39 x42 x44 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 x44 . x43 = x13 x44 ⟶ x39 x42 x43 ⟶ (x39 (x38 (x25 x42 x43 x44) x42) x44 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 . (x39 (x38 (x19 x43 x42) (x20 x43 x42)) x42 ⟶ False) ⟶ (x39 (x19 x43 x42) x43 ⟶ False) ⟶ (x43 = x30 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 x44 . x39 (x19 x44 x43) x44 ⟶ x39 (x38 (x19 x44 x43) x42) x43 ⟶ (x44 = x30 x43 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 x44 x45 . x44 = x30 x45 ⟶ x39 (x38 x42 x43) x45 ⟶ (x39 x42 x44 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 x44 . x43 = x30 x44 ⟶ x39 x42 x43 ⟶ (x39 (x38 x42 (x24 x42 x43 x44)) x44 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 . (x14 x43 x42 = x14 x42 x43 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 . x2 x43 ⟶ x1 x42 x43 ⟶ (x37 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 . x2 x43 ⟶ x1 x42 x43 ⟶ (x6 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x0 x42 ⟶ (x2 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x28 x42 ⟶ x6 x42 ⟶ x37 x42 ⟶ (x4 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x28 x42 ⟶ x6 x42 ⟶ x37 x42 ⟶ (x37 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x28 x42 ⟶ x6 x42 ⟶ x37 x42 ⟶ (x6 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x6 x42 ⟶ x37 x42 ⟶ (x4 x42 ⟶ False) ⟶ (x37 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x6 x42 ⟶ x37 x42 ⟶ (x4 x42 ⟶ False) ⟶ (x6 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x6 x42 ⟶ x37 x42 ⟶ (x4 x42 ⟶ False) ⟶ x28 x42 ⟶ False) ⟶ (∀ x42 . x0 x42 ⟶ x6 x42 ⟶ (x7 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x0 x42 ⟶ x6 x42 ⟶ (x6 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x0 x42 ⟶ x6 x42 ⟶ x37 x42 ⟶ (x4 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x0 x42 ⟶ x6 x42 ⟶ x37 x42 ⟶ (x37 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x0 x42 ⟶ x6 x42 ⟶ x37 x42 ⟶ (x6 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x0 x42 ⟶ x6 x42 ⟶ (x23 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x0 x42 ⟶ x6 x42 ⟶ (x6 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x0 x42 ⟶ x6 x42 ⟶ x37 x42 ⟶ (x33 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x0 x42 ⟶ x6 x42 ⟶ x37 x42 ⟶ (x37 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x0 x42 ⟶ x6 x42 ⟶ x37 x42 ⟶ (x6 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x0 x42 ⟶ (x6 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 . x0 x42 ⟶ (x37 x42 ⟶ False) ⟶ False) ⟶ (∀ x42 x43 . x39 x42 x43 ⟶ x39 x43 x42 ⟶ False) ⟶ (x30 (x40 x22 x21) = x22 ⟶ x13 (x40 x21 x22) = x22 ⟶ False) ⟶ (x21 = x41 ⟶ x40 x22 x21 = x41 ⟶ x40 x21 x22 = x41 ⟶ False) ⟶ False (proof)

Proofgold Asset