Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ο . ∀ x3 . In x3 (Sep2 x0 x1 x2)∀ x4 : ι → ο . (∀ x5 . In x5 x0∀ x6 . In x6 (x1 x5)x2 x5 x6x4 (lam 2 (λ x7 . If_i (x7 = 0) x5 x6)))x4 x3
as obj
-
as prop
67445..Sep2E_impred
theory
HF
stx
89549..
address
TMdp7..Sep2E_impred