Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 (lam x0 x1)In (proj0 x2) x0
as obj
-
as prop
3057f..proj0_Sigma
theory
HF
stx
cbc45..
address
TMG31..proj0_Sigma