Proofgold Proposition

∀ x0 . ∀ x1 : ι → ο . PNoEq_ x0 x1 (λ x2 . and (x1 x2) (x2 = x0 ⟶ ∀ x3 : ο . x3))

type
prop

theory
HotG

name
PNo_extend0_eq

proof
PUQ2Y..

Megalodon
PNo_extend0_eq

proofgold address
TMPWo..^{PNo_extend0_eq}

creator
4903 Pr6Pc../7a7c3..

owner
4903 Pr6Pc../7a7c3..

term root
2d441..