Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 x1 . combinator_equiv (Inj1 (setsum (Inj1 (setsum (Inj0 0) x0)) x1)) x0
as obj
-
as prop
80453..combinator_equiv_K
theory
HF
stx
2b38c..
address
TMdK9..combinator_equiv_K