Proofgold Asset

Definition False := ∀ x0 : ο . x0
Definition not := λ x0 : ο . x0 ⟶ False
Definition nIn := λ x0 x1 . not (prim1 x0 x1)
Definition empty_p := λ x0 . ∀ x1 . nIn x1 x0
Known 0117f.. : ∃ x0 . ∀ x2 . nIn x2 x0
Theorem 438d4.. : ∃ x0 . empty_p x0
Param 4a7ef.. : ι
Known dcd83.. : ∀ x0 . nIn x0 4a7ef..
Theorem 9a431.. : empty_p 4a7ef..
Param iff : ο → ο → ο
Known 0ddd1.. : ∀ x0 x1 . (∀ x2 . iff (prim1 x2 x0) (prim1 x2 x1)) ⟶ x0 = x1
Known iffI : ∀ x0 x1 : ο . (x0 ⟶ x1) ⟶ (x1 ⟶ x0) ⟶ iff x0 x1
Known FalseE : False ⟶ ∀ x0 : ο . x0
Theorem d10d0.. : ∀ x0 . empty_p x0 ⟶ x0 = 4a7ef..
Definition or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition 4326e.. := λ x0 x1 . or (prim1 x1 x0) (and (empty_p x0) (empty_p x1))
Known xm : ∀ x0 : ο . or x0 (not x0)
Known orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Known orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Known andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem f6630.. : ∀ x0 . ∃ x1 . 4326e.. x0 x1
Theorem 25303.. : ∀ x0 x1 . prim1 x1 x0 ⟶ 4326e.. x0 x1
Theorem 9bba6.. : ∀ x0 . empty_p x0 ⟶ 4326e.. x0 4a7ef..
Theorem 7e37c.. : ∀ x0 . not (empty_p x0) ⟶ ∀ x1 . 4326e.. x0 x1 ⟶ prim1 x1 x0
Theorem 6231b.. : ∀ x0 . empty_p x0 ⟶ ∀ x1 . 4326e.. x0 x1 ⟶ x1 = 4a7ef..
Definition c2f57.. := λ x0 : ι → ο . ∃ x1 . ∀ x3 . iff (prim1 x3 x1) (x0 x3)
Param 91630.. : ι → ι
Known fead7.. : ∀ x0 x1 . prim1 x1 (91630.. x0) ⟶ x1 = x0
Known e7a4c.. : ∀ x0 . prim1 x0 (91630.. x0)
Theorem c3a5b.. : ∀ x0 . c2f57.. (4326e.. x0)
Param 707e2.. : (ι → ο) → ι
Known 477e8.. : ∀ x0 : ι → ο . c2f57.. x0 ⟶ ∀ x1 . prim1 x1 (707e2.. x0) ⟶ x0 x1
Known bbc77.. : ∀ x0 : ι → ο . c2f57.. x0 ⟶ ∀ x1 . x0 x1 ⟶ prim1 x1 (707e2.. x0)
Theorem 6c266.. : ∀ x0 . not (empty_p x0) ⟶ 707e2.. (4326e.. x0) = x0