Search for blocks/addresses/...

Proofgold Term Root Disambiguation

λ x0 . λ x1 : ι → ι → ο . λ x2 : ι → ο . λ x3 . lam 4 (λ x4 . If_i (x4 = 0) x0 (If_i (x4 = 1) (encode_r x0 x1) (If_i (x4 = 2) (Sep x0 x2) x3)))
as obj
2575c..
as prop
-
theory
HotG
stx
9a4c8..
address
TMJaQ..