Proofgold Proposition

∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ ∀ x2 : ο . (x0 = x1 ⟶ x2) ⟶ (∀ x3 . x3 ∈ SNoL x1 ⟶ x3 ∈ SNoR x0 ⟶ x2) ⟶ (x0 ∈ SNoL x1 ⟶ x2) ⟶ (x1 ∈ SNoR x0 ⟶ x2) ⟶ (∀ x3 . x3 ∈ SNoR x1 ⟶ x3 ∈ SNoL x0 ⟶ x2) ⟶ (x0 ∈ SNoR x1 ⟶ x2) ⟶ (x1 ∈ SNoL x0 ⟶ x2) ⟶ x2

type
prop

theory
HotG

name
SNoL_or_SNoR_impred

proof
PUcff..

Megalodon
SNoL_or_SNoR_impred

proofgold address
TMKWi..^{SNoL_or_SNoR_impred}

creator
4971 Pr6Pc../28c6f..

owner
4971 Pr6Pc../28c6f..

term root
f8a5e..