Proofgold Address

Param e5b72.. : ι → ι
Definition Subq := λ x0 x1 . ∀ x2 . prim1 x2 x0 ⟶ prim1 x2 x1
Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Param 1216a.. : ι → (ι → ο) → ι
Known andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known set_ext : ∀ x0 x1 . Subq x0 x1 ⟶ Subq x1 x0 ⟶ x0 = x1
Known b2421.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 x0 ⟶ x1 x2 ⟶ prim1 x2 (1216a.. x0 x1)
Known b21da.. : ∀ x0 x1 . prim1 x1 (e5b72.. x0) ⟶ Subq x1 x0
Known ac5c1.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 (1216a.. x0 x1) ⟶ x1 x2
Known d129e.. : ∀ x0 . ∀ x1 : ι → ο . prim1 (1216a.. x0 x1) (e5b72.. x0)
Theorem bda2b.. : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . prim1 x2 (e5b72.. x0) ⟶ prim1 (x1 x2) (e5b72.. x0)) ⟶ (∀ x2 . prim1 x2 (e5b72.. x0) ⟶ ∀ x3 . prim1 x3 (e5b72.. x0) ⟶ Subq x2 x3 ⟶ Subq (x1 x2) (x1 x3)) ⟶ ∀ x2 : ο . (∀ x3 . and (prim1 x3 (e5b72.. x0)) (x1 x3 = x3) ⟶ x2) ⟶ x2 (proof)
Param 94f9e.. : ι → (ι → ι) → ι
Known 3daee.. : ∀ x0 x1 . Subq x1 x0 ⟶ prim1 x1 (e5b72.. x0)
Known 8c6f6.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (94f9e.. x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . prim1 x4 x0 ⟶ x2 = x1 x4 ⟶ x3) ⟶ x3
Theorem 61f1b.. : ∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ prim1 (x2 x3) x1) ⟶ ∀ x3 . prim1 x3 (e5b72.. x0) ⟶ prim1 (94f9e.. x3 x2) (e5b72.. x1) (proof)
Known 696c0.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0 ⟶ prim1 (x1 x2) (94f9e.. x0 x1)
Theorem 13e07.. : ∀ x0 : ι → ι . ∀ x1 x2 . Subq x1 x2 ⟶ Subq (94f9e.. x1 x0) (94f9e.. x2 x0) (proof)
Param 1ad11.. : ι → ι → ι
Known dcf34.. : ∀ x0 x1 . Subq (1ad11.. x0 x1) x0
Theorem 89704.. : ∀ x0 x1 . prim1 (1ad11.. x0 x1) (e5b72.. x0) (proof)
Definition False := ∀ x0 : ο . x0
Definition not := λ x0 : ο . x0 ⟶ False
Definition nIn := λ x0 x1 . not (prim1 x0 x1)
Known 017d4.. : ∀ x0 x1 x2 . prim1 x2 (1ad11.. x0 x1) ⟶ and (prim1 x2 x0) (nIn x2 x1)
Known 753c4.. : ∀ x0 x1 x2 . prim1 x2 x0 ⟶ nIn x2 x1 ⟶ prim1 x2 (1ad11.. x0 x1)
Theorem 60320.. : ∀ x0 x1 x2 . Subq x1 x2 ⟶ Subq (1ad11.. x0 x2) (1ad11.. x0 x1) (proof)
Definition inj := λ x0 x1 . λ x2 : ι → ι . and (∀ x3 . prim1 x3 x0 ⟶ prim1 (x2 x3) x1) (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4)
Param c2e41.. : ι → ι → ο
Param If_i : ο → ι → ι → ι
Param inv : ι → (ι → ι) → ι → ι
Definition bij := λ x0 x1 . λ x2 : ι → ι . and (and (∀ x3 . prim1 x3 x0 ⟶ prim1 (x2 x3) x1) (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4)) (∀ x3 . prim1 x3 x1 ⟶ ∀ x4 : ο . (∀ x5 . and (prim1 x5 x0) (x2 x5 = x3) ⟶ x4) ⟶ x4)
Known c6ad4.. : ∀ x0 x1 . ∀ x2 : ι → ι . bij x0 x1 x2 ⟶ c2e41.. x0 x1
Known and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Definition or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known xm : ∀ x0 : ο . or x0 (not x0)
Known If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0 ⟶ If_i x0 x1 x2 = x1
Known f775d.. : ∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4) ⟶ ∀ x3 . prim1 x3 x0 ⟶ inv x0 x2 (x2 x3) = x3
Known 26c23.. : ∀ x0 x1 x2 . prim1 x2 (1ad11.. x0 x1) ⟶ prim1 x2 x0
Known If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0 ⟶ If_i x0 x1 x2 = x2
Known FalseE : False ⟶ ∀ x0 : ο . x0
Theorem c698c.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι . inj x0 x1 x2 ⟶ inj x1 x0 x3 ⟶ c2e41.. x0 x1 (proof)