Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 . RealsStruct x0∀ x1 . x1field0 x0∀ x2 . x2field0 x0RealsStruct_leq x0 (field4 x0) (field1b x0 (field2b x0 x1 x1) (field2b x0 x2 x2))
as obj
-
as prop
e739f..RealsStruct_sum_squares_nonneg
theory
HotG
stx
56719..
address
TMFA9..RealsStruct_sum_squares_nonneg