Proofgold Term Root Disambiguation

∀ x0 . nat_p x0 ⟶ ∀ x1 . In x1 x0 ⟶ ∀ x2 . nat_p x2 ⟶ In (add_nat x2 x1) (add_nat x2 x0)

as obj
-

as prop
428f7..^add_nat_ltR

theory
HF

stx
e311e..

address
TMRE3..^add_nat_ltR