Proofgold Term Root Disambiguation

∀ x0 : ι → ι → ο . (∀ x1 . ∃ x2 . x0 x1 x2) ⟶ ∃ x1 : ι → ι . ∀ x3 . x0 x3 (x1 x3)

as obj
-

as prop
99a65..^Skolem_0

theory
HF

stx
a8b20..

address
TMFHf..^Skolem_0