Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 . ∀ x1 : ι → ι . ∀ x2 . In x2 (Pi x0 x1)∀ x3 . In x3 (Pi x0 x1)(∀ x4 . In x4 x0Subq (ap x2 x4) (ap x3 x4))Subq x2 x3
as obj
-
as prop
44e63..Pi_ext_Subq
theory
HF
stx
89549..
address
TMaWq..Pi_ext_Subq