Proofgold Proposition

∀ x0 . RealsStruct x0 ⟶ RealsStruct_Q x0 = {x2 ∈ field0 x0|∀ x3 : ο . (∀ x4 . and (x4 ∈ {x5 ∈ field0 x0|or (or (explicit_Field_minus (field0 x0) (field4 x0) (RealsStruct_one x0) (field1b x0) (field2b x0) x5 ∈ RealsStruct_Npos x0) (x5 = field4 x0)) (x5 ∈ RealsStruct_Npos x0)}) (∀ x5 : ο . (∀ x6 . and (x6 ∈ RealsStruct_Npos x0) (field2b x0 x6 x2 = x4) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3}

type
prop

theory
HotG

name
-

proof
PUSVY..

Megalodon
-

proofgold address
TMS8k..

creator
5804 Pr6Pc../ecd5b..

owner
5804 Pr6Pc../ecd5b..

term root
61f0c..