Proofgold Proposition

∀ x0 x1 x2 . nat_p x0 ⟶ x1 ∈ ordsucc x0 ⟶ nat_p x2 ⟶ nat_p x1 ⟶ exactly1of2 (SetAdjoin x1 (Sing 1) ∈ eps_ x0) (x1 ∈ eps_ x0)

type
prop

theory
HotG

name
-

proof
PUTNo..

Megalodon
Conj_SNo__eps___3__3

proofgold address
TMTRS..^{Conj_SNo__eps___3__3}

creator
35053 PrNpY../70ca8..

owner
35061 PrNpY../da3c3..

term root
4bca0..