Proofgold Proposition

∀ x0 x1 x2 . x2 ∈ setprod x0 x1 ⟶ proj1 x2 ∈ x1

type
prop

theory
HotG

name
proj1_setprod

proof
PUdQg..

Megalodon
proj1_setprod

proofgold address
TMVQE..^{proj1_setprod}

creator
4899 Pr6Pc../8d2ba..

owner
4899 Pr6Pc../8d2ba..

term root
f6765..