Proofgold Term Root Disambiguation

∀ x0 . x0 ∈ omega ⟶ ∀ x1 . x1 ∈ omega ⟶ add_nat x0 x1 = 0 ⟶ and (x0 = 0) (x1 = 0)

as obj
-

as prop
2e6cb..^{add_nat_0_inv}

theory
HotG

stx
7fa67..

address
TMKXC..^{add_nat_0_inv}