Proofgold Proposition

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

type
prop

theory
HoTg

name
PNo_extend0_eq

proof
PUdWB..

Megalodon
-

proofgold address
TMRAJ..

creator
2791 PrGxv../42187..

owner
2791 PrGxv../42187..

term root
2d441..