const CSNo : set prop const mul_CSNo : set set set axiom CSNo_mul_CSNo: !x:set.!y:set.CSNo x -> CSNo y -> CSNo (mul_CSNo x y) lemma !x:set.!y:set.!z:set.CSNo x -> CSNo y -> CSNo z -> CSNo (mul_CSNo y z) -> mul_CSNo x (mul_CSNo y z) = mul_CSNo (mul_CSNo x y) z claim !x:set.!y:set.!z:set.CSNo x -> CSNo y -> CSNo z -> mul_CSNo x (mul_CSNo y z) = mul_CSNo (mul_CSNo x y) z