Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 x1 x2 x3 . lam 2 (λ x5 . If_i (x5 = 0) x0 x1) = lam 2 (λ x5 . If_i (x5 = 0) x2 x3)∀ x4 : ο . (x0 = x2x1 = x3x4)x4
as obj
-
as prop
abe40..tuple_2_inj_impred
theory
HF
stx
89549..
address
TMb4D..tuple_2_inj_impred