Proofgold Proposition

∀ x0 . ordinal x0 ⟶ ∀ x1 . In x1 x0 ⟶ ∀ x2 x3 . SNoEq_ x0 x2 x3 ⟶ SNoEq_ x1 x2 x3

type
prop

theory
HF

name
-

proof
PUQ8e..

Megalodon
SNoEq_antimon_

proofgold address
TMWhP..^{SNoEq_antimon_}

creator
2357 PrGxv../21874..

owner
2357 PrGxv../21874..

term root
3d966..