Proofgold Proposition

∀ x0 . x0 ⊆ SNoS_ omega ⟶ ∀ x1 . x1 ⊆ SNoS_ omega ⟶ SNoCutP x0 x1 ⟶ SNoLev (SNoCut x0 x1) ∈ ordsucc omega

type
prop

theory
HotG

name
SNoCutP_SNoCut_omega

proof
PUgvb..

Megalodon
SNoCutP_SNoCut_omega

proofgold address
TMaV1..^{SNoCutP_SNoCut_omega}

creator
12283 PrGxv../3d314..

owner
12283 PrGxv../3d314..

term root
d1161..