Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 . ∀ x1 : ι → ι . ∀ x2 . iff (x2Pi x0 x1) (and (∀ x3 . x3x2and (pair_p x3) (ap x3 0x0)) (∀ x3 . x3x0ap x2 x3x1 x3))
as obj
-
as prop
e80f9..PiEq
theory
HotG
stx
08e38..
address
TMLoc..PiEq