Proofgold Term Root Disambiguation

∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ add_SNo (minus_SNo (ordsucc x0)) (ordsucc x1) = add_SNo (minus_SNo x0) x1

as obj
-

as prop
bd5ca..

theory
HotG

stx
33c6f..

address
TMM64..