Proofgold Term Root Disambiguation

λ x0 x1 . ∀ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x2 ⟶ Church13_p x3 ⟶ x0 = x2 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 ⟶ x1 = x3 0 u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12 ⟶ TwoRamseyGraph_3_5_Church13 x2 x3 = λ x5 x6 . x5

as obj
511fc..

as prop
-

theory
HotG

stx
62734..

address
TMHw8..