Proofgold Proposition

∀ x0 x1 . OSNo x0 ⟶ OSNo x1 ⟶ OSNo_proj0 x0 = OSNo_proj0 x1 ⟶ OSNo_proj1 x0 = OSNo_proj1 x1 ⟶ x0 = x1

type
prop

theory
HotG

name
OSNo_proj0proj1_split

proof
PUdK2..

Megalodon
OSNo_proj0proj1_split

proofgold address
TMHn7..^{OSNo_proj0proj1_split}

creator
28513 PrQUS../73178..

owner
28513 PrQUS../73178..

term root
9e9a0..