Search for blocks/addresses/...

Proofgold Term Root Disambiguation

λ x0 . λ x1 : ι → ι → ι . λ x2 . prim0 (λ x3 . and (prim1 x3 x0) (and (x1 x2 x3 = explicit_Group_identity x0 x1) (x1 x3 x2 = explicit_Group_identity x0 x1)))
as obj
ff23b..
as prop
-
theory
HoTg
stx
4b82f..
address
TMHFM..explicit_Group_inverse