Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 . ∀ x1 : ι → ι . ∀ x2 : ι → ι → ι . ∀ x3 . In x3 x0∀ x4 . In x4 (x1 x3)∀ x5 . In x5 (x2 x3 x4)In (lam 2 (λ x6 . If_i (x6 = 0) x3 (lam 2 (λ x7 . If_i (x7 = 0) x4 x5)))) (lam2 x0 x1 x2)
as obj
-
as prop
d46d7..lam2_I2
theory
HF
stx
b6147..
address
TMcH1..lam2_I2