Proofgold Proposition

∀ x0 : ι → ι . ∀ x1 . nat_p x1 ⟶ (∀ x2 . x2 ∈ x1 ⟶ nat_p (x0 x2)) ⟶ Pi_nat x0 x1 = 0 ⟶ ∀ x2 : ο . (∀ x3 . and (x3 ∈ x1) (x0 x3 = 0) ⟶ x2) ⟶ x2

type
prop

theory
HotG

name
Pi_nat_0_inv

proof
PUPh4..

Megalodon
Pi_nat_0_inv

proofgold address
TMR4r..^Pi_nat_0_inv

creator
29757 PrQUS../12189..

owner
29757 PrQUS../12189..

term root
688c9..