Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 x1 . Subq x0 x1∀ x2 x3 : ι → ι . (∀ x4 . In x4 x0Subq (x2 x4) (x3 x4))Subq (lam x0 x2) (lam x1 x3)
as obj
-
as prop
1587f..Sigma_mon
theory
HF
stx
cbc45..
address
TMNp7..Sigma_mon