Proofgold Term Root Disambiguation

∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ SNoLe 1 (add_SNo x0 (minus_SNo x1)) ⟶ SNoLe (add_SNo x1 (minus_SNo x0)) (minus_SNo 1)

as obj
-

as prop
afbec..^{minus_SNo_Le_swap_1}

theory
HotG

stx
5fba1..

address
TMKn5..^{minus_SNo_Le_swap_1}