Proofgold Proposition

∀ x0 . nat_p x0 ⟶ ∀ x1 . nat_p x1 ⟶ ∀ x2 x3 . equip x2 x0 ⟶ equip x3 x1 ⟶ equip (setsum x2 x3) (add_nat x0 x1)

type
prop

theory
HF

name
-

proof
PUVGM..

Megalodon
equip_setsum_add_nat_2

proofgold address
TMQsC..^{equip_setsum_add_nat_2}

creator
2277 PrGxv../8bb61..

owner
2277 PrGxv../8bb61..

term root
10a83..