Proofgold Proposition

∀ x0 x1 x2 . ∀ x3 : ι → ι . ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x2 ⟶ mul_SNo (add_SNo 1 (mul_SNo (add_SNo x5 (minus_SNo x1)) x4)) (x3 x5) ∈ SNo_recipauxset x0 x1 x2 x3

type
prop

theory
HotG

name
SNo_recipauxset_I

proof
PUewm..

Megalodon
SNo_recipauxset_I

proofgold address
TMUCP..^{SNo_recipauxset_I}

creator
27779 PrQUS../825f2..

owner
27779 PrQUS../825f2..

term root
fb23e..