Proofgold Proposition

(∀ x0 x1 x2 x3 x4 . (∀ x5 . x5 ∈ x1 ⟶ SNo x5) ⟶ SNo (SNoCut x0 x1) ⟶ (∀ x5 . x5 ∈ x1 ⟶ SNoLt (SNoCut x0 x1) x5) ⟶ (∀ x5 . SNo x5 ⟶ (∀ x6 . x6 ∈ x0 ⟶ SNoLt x6 x5) ⟶ (∀ x6 . x6 ∈ x1 ⟶ SNoLt x5 x6) ⟶ and (SNoLev (SNoCut x0 x1) ⊆ SNoLev x5) (SNoEq_ (SNoLev (SNoCut x0 x1)) (SNoCut x0 x1) x5)) ⟶ SNo x4 ⟶ SNoLt x4 (SNoCut x0 x1) ⟶ (∀ x5 . x5 ∈ x0 ⟶ SNoLt x5 x4) ⟶ not (∀ x5 . x5 ∈ x1 ⟶ SNoLt x4 x5)) ⟶ ∀ x0 : ο . x0

type
prop

theory
HotG

name
-

proof
PUfXk..

Megalodon
-

proofgold address
TMUPq..

creator
35087 PrNpY../58164..

owner
35087 PrNpY../58164..

term root
95737..