Search for blocks/addresses/...

Proofgold Term Root Disambiguation

hf term
(object) array( 'type' => 'termroot', 'hfbuiltin' => true, 'trmpres' => 'Inj1 = In_rec_poly_i (λ x1 . λ x2 : ι → ι . binunion (Sing 0) (Repl x1 x2))', )
address
TMMGu..Inj1_def