Proofgold Term Root Disambiguation

∀ x0 . HSNo x0 ⟶ ∀ x1 . nat_p x1 ⟶ HSNo (exp_HSNo_nat x0 x1)

as obj
-

as prop
cfcd3..^{HSNo_exp_HSNo_nat}

theory
HotG

stx
43801..

address
TMUMi..^{HSNo_exp_HSNo_nat}