Proofgold Address

Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Definition empty_p := λ x0 . ∀ x1 . nIn x1 x0
Definition 41dcb.. := λ x0 . not (empty_p x0)
Definition boolToProp := prim1 0
Param If_i^If_i : ο → ι → ι → ι
Param ordsucc^ordsucc : ι → ι
Definition propToBool := λ x0 : ο . If_i x0 1 0
Param nat_p^nat_p : ι → ο
Param omega^omega : ι
Known nat_0^nat_0 : nat_p 0
Known nat_p_omega^nat_p_omega : ∀ x0 . nat_p x0 ⟶ x0 ∈ omega
Theorem e4648.. : 0 ∈ omega (proof)
Theorem 30796.. : 41dcb.. omega (proof)
Param Pi^Pi : ι → (ι → ι) → ι
Definition setexp^setexp := λ x0 x1 . Pi x1 (λ x2 . x0)
Param ap^ap : ι → ι → ι
Known ap_Pi^ap_Pi : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . x2 ∈ Pi x0 x1 ⟶ x3 ∈ x0 ⟶ ap x2 x3 ∈ x1 x3
Theorem 67069.. : ∀ x0 x1 x2 . x2 ∈ setexp x1 x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ap x2 x3 ∈ x1 (proof)
Theorem 69857.. : ∀ x0 x1 x2 x3 . x3 ∈ setexp (setexp x2 x1) x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x1 ⟶ ap (ap x3 x4) x5 ∈ x2 (proof)
Known dneg^dneg : ∀ x0 : ο . not (not x0) ⟶ x0
Theorem 799d0.. : ∀ x0 . 41dcb.. x0 ⟶ ∀ x1 : ο . (∀ x2 . x2 ∈ x0 ⟶ x1) ⟶ x1 (proof)
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known xm^xm : ∀ x0 : ο . or x0 (not x0)
Known If_i_1^If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0 ⟶ If_i x0 x1 x2 = x1
Known In_1_2^In_1_2 : 1 ∈ 2
Known If_i_0^If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0 ⟶ If_i x0 x1 x2 = x2
Known In_0_2^In_0_2 : 0 ∈ 2
Theorem 3072f.. : ∀ x0 : ο . propToBool x0 ∈ 2 (proof)
Known cases_2^cases_2 : ∀ x0 . x0 ∈ 2 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 1 ⟶ x1 x0
Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Known EmptyE^EmptyE : ∀ x0 . nIn x0 0
Theorem 7dcbe.. : ∀ x0 . x0 ∈ 2 ⟶ boolToProp x0 ⟶ x0 = 1 (proof)
Known In_0_1^In_0_1 : 0 ∈ 1
Theorem 9be3e.. : ∀ x0 . x0 ∈ 2 ⟶ not (boolToProp x0) ⟶ x0 = 0 (proof)
Theorem a673a.. : ∀ x0 : ο . x0 ⟶ boolToProp (propToBool x0) (proof)
Theorem b1ad2.. : ∀ x0 : ο . boolToProp (propToBool x0) ⟶ x0 (proof)