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

Proofgold Asset