Proofgold Proposition

∀ x0 x1 . nat_p x0 ⟶ nat_p x1 ⟶ ∀ x2 . In x2 x0 ⟶ ∀ x3 . In x3 x1 ⟶ In (add_nat x2 (mul_nat x3 x0)) (mul_nat x0 x1)

type
prop

theory
HF

name
-

proof
PUZkx..

Megalodon
add_mul_nat_lt

proofgold address
TMFSF..^{add_mul_nat_lt}

creator
2364 PrGxv../c3029..

owner
2364 PrGxv../c3029..

term root
93c24..