Proofgold Term Root Disambiguation

∀ x0 . ∀ x1 x2 x3 : ι → ι . infinite x0 ⟶ (∀ x4 . x4 ⊆ x0 ⟶ infinite x4 ⟶ and (x1 x4 ⊆ x4) (infinite (x1 x4))) ⟶ (∀ x4 . x4 ⊆ x0 ⟶ infinite x4 ⟶ and (x2 x4 ∈ x4) (nIn (x2 x4) (x1 x4))) ⟶ x3 0 = x1 x0 ⟶ (∀ x4 . nat_p x4 ⟶ x3 (ordsucc x4) = x1 (x3 x4)) ⟶ and (and (∀ x4 . nat_p x4 ⟶ and (x3 x4 ⊆ x0) (infinite (x3 x4))) (∀ x4 . x4 ∈ omega ⟶ ∀ x5 . x5 ∈ omega ⟶ x4 ⊆ x5 ⟶ x3 x5 ⊆ x3 x4)) (∀ x4 . x4 ∈ omega ⟶ ∀ x5 . x5 ∈ omega ⟶ x2 (x3 x4) = x2 (x3 x5) ⟶ x4 = x5)

as obj
-

as prop
c1cc5..^{infiniteRamsey_lem}

theory
HotG

stx
afc5a..

address
TMcTq..^{infiniteRamsey_lem}