Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 . nat_p x0∀ x1 : ι → ι . (∀ x2 . x2x0nat_p (x1 x2))∀ x2 . x2x0divides_nat (x1 x2) (nat_primrec 1 (λ x3 . mul_nat (x1 x3)) x0)
as obj
-
as prop
4c147..
theory
HotG
stx
71eda..
address
TMGSR..