Search for blocks/addresses/...

Proofgold Term Root Disambiguation

λ x0 x1 . and (and (struct_b x1) (struct_b x0)) (unpack_b_o x1 (λ x2 . λ x3 : ι → ι → ι . unpack_b_o x0 (λ x4 . λ x5 : ι → ι → ι . and (and (x0 = pack_b x4 x3) (Group (pack_b x4 x3))) (x4x2))))
as obj
cb09c..subgroup
as prop
-
theory
HotG
stx
a0c68..
address
TMLRk..subgroup