Proofgold Proposition

∀ x0 x1 . Sing 2 ∈ x0 ⟶ ordinal x1 ⟶ not (Sing 2 ∈ SetAdjoin x1 (Sing 1))

type
prop

theory
HotG

name
-

proof
PUTNo..

Megalodon
Conj_ctagged_eqE_Subq__1__1

proofgold address
TMTfP..^{Conj_ctagged_eqE_Subq__1__1}

creator
35053 PrNpY../40ab5..

owner
35061 PrNpY../789d7..

term root
cfbd0..