Proofgold Term Root Disambiguation

∀ x0 . nat_p x0 ⟶ even_nat (mul_nat 2 x0)

as obj
-

as prop
506d4..^{even_nat_double}

theory
HotG

stx
80e8e..

address
TMG3Z..^{even_nat_double}