Proofgold Term Root Disambiguation

∀ x0 . x0 ∈ u17 ⟶ ∀ x1 . x1 ∈ u17 ⟶ u17_to_Church17 x0 = u17_to_Church17 x1 ⟶ x0 = x1

as obj
-

as prop
fda94..

theory
HotG

stx
f13be..

address
TMa8G..