Proofgold Term Root Disambiguation

∀ x0 . In 0 x0 ⟶ ∀ x1 . nat_p x1 ⟶ ∀ x2 . In x2 x1 ⟶ Subq (setexp x0 x2) (setexp x0 x1)

as obj
-

as prop
5ac7b..^{nat_in_setexp_mon}

theory
HF

stx
89549..

address
TMdoa..^{nat_in_setexp_mon}