Proofgold Term Root Disambiguation

∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ ∀ x2 . infinite x2 ⟶ ∀ x3 : ι → ι . (∀ x4 . x4 ⊆ x2 ⟶ equip x4 x1 ⟶ x3 x4 ∈ x0) ⟶ ∃ x4 . and (x4 ⊆ x2) (∃ x6 . and (x6 ∈ x0) (and (infinite x4) (∀ x8 . x8 ⊆ x4 ⟶ equip x8 x1 ⟶ x3 x8 = x6)))

as obj
-

as prop
865fc..^{infiniteRamsey}

theory
HotG

stx
7d5aa..

address
TMH9R..^{infiniteRamsey}