Proofgold Proposition

∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ SetAdjoin x0 (Sing 1) = SetAdjoin x1 (Sing 1) ⟶ x0 = x1

type
prop

theory
HotG

name
tagged_eqE_eq

proof
PUUwp..

Megalodon
tagged_eqE_eq

proofgold address
TMYDs..^{tagged_eqE_eq}

creator
4910 Pr6Pc../8dd97..

owner
4910 Pr6Pc../8dd97..

term root
1f7dc..