Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 x1 . nat_p x1exp_CSNo_nat x0 (ordsucc x1) = mul_CSNo x0 (exp_CSNo_nat x0 x1)
as obj
-
as prop
ce5d5..exp_CSNo_nat_S
theory
HotG
stx
5ed1a..
address
TMTso..exp_CSNo_nat_S