Proofgold Term Root Disambiguation

∀ x0 . nat_p x0 ⟶ ∀ x1 . In x1 x0 ⟶ ∀ x2 . nat_p x2 ⟶ In (mul_nat x1 (ordsucc x2)) (mul_nat x0 (ordsucc x2))

as obj
-

as prop
d3280..^mul_nat_ltL

theory
HF

stx
b2d3f..

address
TMQQd..^mul_nat_ltL