Proofgold Proposition

∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ x0 ⊆ x1 ⟶ ∃ x2 . and (nat_p x2) (x1 = add_nat x2 x0)

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..