Proofgold Address

Param nat_p^nat_p : ι → ο
Param equip^equip : ι → ι → ο
Param ordsucc^ordsucc : ι → ι
Param and^and : ο → ο → ο
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Known dneg^dneg : ∀ x0 : ο . not (not x0) ⟶ x0
Param atleastp^atleastp : ι → ι → ο
Known 4fb58..^{Pigeonhole_not_atleastp_ordsucc} : ∀ x0 . nat_p x0 ⟶ not (atleastp (ordsucc x0) x0)
Known atleastp_tra^atleastp_tra : ∀ x0 x1 x2 . atleastp x0 x1 ⟶ atleastp x1 x2 ⟶ atleastp x0 x2
Known equip_atleastp^{equip_atleastp} : ∀ x0 x1 . equip x0 x1 ⟶ atleastp x0 x1
Known equip_sym^equip_sym : ∀ x0 x1 . equip x0 x1 ⟶ equip x1 x0
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Known Subq_atleastp^{Subq_atleastp} : ∀ x0 x1 . x0 ⊆ x1 ⟶ atleastp x0 x1
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known ReplI^ReplI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ x1 x2 ∈ prim5 x0 x1
Known equip_tra^equip_tra : ∀ x0 x1 x2 . equip x0 x1 ⟶ equip x1 x2 ⟶ equip x0 x2
Known d2050.. : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 = x1 x3 ⟶ x2 = x3) ⟶ equip x0 (prim5 x0 x1)
Theorem 07015.. : ∀ x0 . ∀ x1 : ι → ι → ο . ∀ x2 . nat_p x2 ⟶ equip x0 (ordsucc x2) ⟶ ∀ x3 . equip x3 x2 ⟶ ∀ x4 : ι → ι . (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x0 ⟶ x1 x6 x5 ⟶ x6 = x4 x5) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ x4 x5 = x4 x6 ⟶ x5 = x6) ⟶ ∀ x5 : ο . (∀ x6 . and (x6 ∈ x0) (∀ x7 . x7 ∈ x3 ⟶ not (x1 x6 x7)) ⟶ x5) ⟶ x5 (proof)
Theorem 21e21.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x2 x3 ⟶ x1 x3 x2) ⟶ ∀ x2 . nat_p x2 ⟶ equip x0 (ordsucc x2) ⟶ ∀ x3 . equip x3 x2 ⟶ ∀ x4 : ι → ι . (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x0 ⟶ x1 x6 x5 ⟶ x6 = x4 x5) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ x4 x5 = x4 x6 ⟶ x5 = x6) ⟶ ∀ x5 : ο . (∀ x6 . and (x6 ∈ x0) (∀ x7 . x7 ∈ x3 ⟶ not (x1 x6 x7)) ⟶ x5) ⟶ x5 (proof)