Search for blocks/addresses/...

Proofgold Term Root Disambiguation

λ x0 x1 . λ x2 : ι → ι . nat_primrec 0 (λ x3 x4 . If_i (x3x0) 0 (add_CSNo (x2 x3) x4)) (ordsucc x1)
as obj
81ddb..Sum
as prop
-
theory
HotG
stx
a3ed2..
address
TMFy5..Sum