Proofgold Term Root Disambiguation

∀ x0 : ι → ι . ∀ x1 . nat_p x1 ⟶ finite_add_SNo (ordsucc x1) x0 = add_SNo (finite_add_SNo x1 x0) (x0 x1)

as obj
-

as prop
73a8e..

theory
HotG

stx
6036f..

address
TMU9W..