const CSNo : set prop const SNo : set prop const CSNo_Im : set set axiom CSNo_ImR: !x:set.CSNo x -> SNo (CSNo_Im x) const mul_CSNo : set set set const CSNo_Re : set set lemma !x:set.!y:set.!z:set.CSNo x -> CSNo y -> CSNo z -> CSNo (mul_CSNo y z) -> CSNo (mul_CSNo x y) -> CSNo (mul_CSNo x (mul_CSNo y z)) -> CSNo (mul_CSNo (mul_CSNo x y) z) -> SNo (CSNo_Re x) -> SNo (CSNo_Re y) -> SNo (CSNo_Re z) -> SNo (CSNo_Im x) -> SNo (CSNo_Im y) -> SNo (CSNo_Im z) -> mul_CSNo x (mul_CSNo y z) = mul_CSNo (mul_CSNo x y) z var x:set var y:set var z:set hyp CSNo x hyp CSNo y hyp CSNo z hyp CSNo (mul_CSNo y z) hyp CSNo (mul_CSNo x y) hyp CSNo (mul_CSNo x (mul_CSNo y z)) hyp CSNo (mul_CSNo (mul_CSNo x y) z) hyp SNo (CSNo_Re x) hyp SNo (CSNo_Re y) hyp SNo (CSNo_Re z) hyp SNo (CSNo_Im x) claim SNo (CSNo_Im y) -> mul_CSNo x (mul_CSNo y z) = mul_CSNo (mul_CSNo x y) z