Proofgold Proposition

∀ x0 . nat_p x0 ⟶ ∀ x1 . In x1 x0 ⟶ ∀ x2 . nat_p x2 ⟶ In (mul_nat (ordsucc x2) x1) (mul_nat (ordsucc x2) x0)

type
prop

theory
HF

name
-

proof
PUZkx..

Megalodon
mul_nat_ltR

proofgold address
TMX3q..^mul_nat_ltR

creator
2364 PrGxv../7a5d7..

owner
2364 PrGxv../7a5d7..

term root
4af03..