Proofgold Asset

Known 128d8.. : ∀ x0 x1 x2 x3 . prim0 x0 x1 = prim0 x2 x3 ⟶ ∀ x4 : ο . (x0 = x2 ⟶ x1 = x3 ⟶ x4) ⟶ x4
Theorem 50787.. : ∀ x0 x1 x2 x3 . prim0 x0 x1 = prim0 x2 x3 ⟶ x0 = x2 (proof)
Theorem 93754.. : ∀ x0 x1 x2 x3 . prim0 x0 x1 = prim0 x2 x3 ⟶ x1 = x3 (proof)
Definition False := ∀ x0 : ο . x0
Known 9aea6.. : ∀ x0 x1 . ∀ x2 : ι → ι . prim0 x0 x1 = prim1 x2 ⟶ ∀ x3 : ο . x3
Theorem 92e6a.. : ∀ x0 : ι → ι . ∀ x1 x2 . prim1 x0 = prim0 x1 x2 ⟶ False (proof)
Known b4755.. : ∀ x0 x1 : ι → ι . prim1 x0 = prim1 x1 ⟶ x0 = x1
Theorem db6fe.. : ∀ x0 x1 : ι → ι . ∀ x2 . prim1 x0 = prim1 x1 ⟶ x0 x2 = x1 x2 (proof)
Definition 236c6.. := prim1 (λ x0 . x0)
Known f558c.. : ∀ x0 x1 . 236c6.. = prim0 x0 x1 ⟶ ∀ x2 : ο . x2
Theorem 0286c.. : ∀ x0 x1 . prim0 x0 x1 = 236c6.. ⟶ False (proof)
Known 148f8.. : ∀ x0 : ι → ι → ι . 236c6.. = prim1 (λ x2 . prim1 (x0 x2)) ⟶ ∀ x1 : ο . x1
Theorem 2042d.. : ∀ x0 : ι → ι → ι . prim1 (λ x2 . prim1 (x0 x2)) = 236c6.. ⟶ False (proof)
Known f2c23.. : ∀ x0 x1 : ι → ι . 236c6.. = prim1 (λ x3 . prim0 (x0 x3) (x1 x3)) ⟶ ∀ x2 : ο . x2
Theorem 48046.. : ∀ x0 x1 : ι → ι . prim1 (λ x3 . prim0 (x0 x3) (x1 x3)) = 236c6.. ⟶ False (proof)
Known 61590.. : 236c6.. = prim1 (λ x1 . 236c6..) ⟶ False
Theorem 732ef.. : prim1 (λ x1 . 236c6..) = 236c6.. ⟶ False (proof)