Proofgold Proposition

∀ x0 . nat_p x0 ⟶ (x0 = 1 ⟶ ∀ x1 : ο . x1) ⟶ ∀ x1 . x1 ∈ x0 ⟶ ordsucc (mul_nat x1 x1) ∈ mul_nat x0 x0

type
prop

theory
HotG

name
-

proof
PUTs8..

Megalodon
-

proofgold address
TMSvi..

creator
29423 Pr5Zc../447c6..

owner
29423 Pr5Zc../447c6..

term root
ea9c6..