Proofgold Proposition

∀ x0 . ordinal x0 ⟶ ∀ x1 : ι → ο . PNoEq_ x0 x1 (PNo_pred (PNoCutL x0 x1) (PNoCutR x0 x1))

type
prop

theory
HotG

name
PNoCut_pred_eq

proof
PUQ2Y..

Megalodon
PNoCut_pred_eq

proofgold address
TMRmN..^{PNoCut_pred_eq}

creator
4903 Pr6Pc../f0a1f..

owner
4903 Pr6Pc../f0a1f..

term root
3c549..