Proofgold Term Root Disambiguation

λ x0 : ο . If_i x0 (4ae4a.. 4a7ef..) 4a7ef..

as obj
896e2..

as prop
-

theory
HoTg

stx
aca54..

address
TMXVn..