Proofgold Proposition

∀ x0 x1 . 02b90.. x0 x1 ⟶ ∀ x2 : ο . (80242.. (02a50.. x0 x1) ⟶ prim1 (e4431.. (02a50.. x0 x1)) (4ae4a.. (0ac37.. (a842e.. x0 (λ x3 . 4ae4a.. (e4431.. x3))) (a842e.. x1 (λ x3 . 4ae4a.. (e4431.. x3))))) ⟶ (∀ x3 . prim1 x3 x0 ⟶ 099f3.. x3 (02a50.. x0 x1)) ⟶ (∀ x3 . prim1 x3 x1 ⟶ 099f3.. (02a50.. x0 x1) x3) ⟶ (∀ x3 . 80242.. x3 ⟶ (∀ x4 . prim1 x4 x0 ⟶ 099f3.. x4 x3) ⟶ (∀ x4 . prim1 x4 x1 ⟶ 099f3.. x3 x4) ⟶ and (Subq (e4431.. (02a50.. x0 x1)) (e4431.. x3)) (SNoEq_ (e4431.. (02a50.. x0 x1)) (02a50.. x0 x1) x3)) ⟶ x2) ⟶ x2

type
prop

theory
HoTg

name
-

proof
PUTG4..

Megalodon
-

proofgold address
TMJfy..

creator
3831 PrGxv../cf03e..

owner
3831 PrGxv../cf03e..

term root
b01da..