Proofgold Term Root Disambiguation

∀ 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

as obj
-

as prop
68ba9..^{SNoL_or_SNoR_impred}

theory
HotG

stx
fd8fe..

address
TMKsC..^{SNoL_or_SNoR_impred}