Proofgold Term Root Disambiguation

∀ x0 . x0 ∈ u17 ⟶ ∀ x1 . x1 ∈ u17 ⟶ (TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x0) (u17_to_Church17 x1) = λ x3 x4 . x3) ⟶ TwoRamseyGraph_3_6_17 x0 x1

as obj
-

as prop
d0d1e..

theory
HotG

stx
a2673..

address
TMYMB..