Proofgold Proposition

∀ x0 x1 . OSNo x0 ⟶ OSNo x1 ⟶ conj_OSNo (mul_OSNo x0 x1) = mul_OSNo (conj_OSNo x1) (conj_OSNo x0)

type
prop

theory
HotG

name
conj_mul_OSNo

proof
PUdK2..

Megalodon
conj_mul_OSNo

proofgold address
TMNPP..^{conj_mul_OSNo}

creator
28513 PrQUS../285e7..

owner
28513 PrQUS../285e7..

term root
05d74..