Proofgold Proposition

∀ x0 x1 x2 . SNo x0 ⟶ (x0 = 0 ⟶ ∀ x3 : ο . x3) ⟶ SNo x1 ⟶ SNo x2 ⟶ mul_SNo x0 x1 = mul_SNo x0 x2 ⟶ x1 = x2

type
prop

theory
HotG

name
mul_SNo_nonzero_cancel

proof
PUUxZ..

Megalodon
mul_SNo_nonzero_cancel_L

proofgold address
TMdbR..^{mul_SNo_nonzero_cancel_L}

creator
12264 PrGxv../75bbf..

owner
12264 PrGxv../75bbf..

term root
67c26..