Proofgold Proposition

∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ x0 ⊆ x1 ⟶ ∀ x2 : ο . (∀ x3 . and (nat_p x3) (x1 = add_nat x3 x0) ⟶ x2) ⟶ x2

type
prop

theory
HotG

name
nat_Subq_add_ex

proof
PUewm..

Megalodon
nat_Subq_add_ex

proofgold address
TMYgM..^{nat_Subq_add_ex}

creator
27779 PrQUS../63c36..

owner
27779 PrQUS../63c36..

term root
a1e40..