const CSNo : set prop const add_CSNo : set set set axiom CSNo_add_CSNo: !x:set.!y:set.CSNo x -> CSNo y -> CSNo (add_CSNo x y) const mul_CSNo : set set set lemma !x:set.!y:set.!z:set.CSNo x -> CSNo y -> CSNo z -> CSNo (add_CSNo y z) -> CSNo (mul_CSNo x y) -> CSNo (mul_CSNo x z) -> CSNo (mul_CSNo x (add_CSNo y z)) -> CSNo (add_CSNo (mul_CSNo x y) (mul_CSNo x z)) -> mul_CSNo x (add_CSNo y z) = add_CSNo (mul_CSNo x y) (mul_CSNo x z) var x:set var y:set var z:set hyp CSNo x hyp CSNo y hyp CSNo z hyp CSNo (add_CSNo y z) hyp CSNo (mul_CSNo x y) hyp CSNo (mul_CSNo x z) claim CSNo (mul_CSNo x (add_CSNo y z)) -> mul_CSNo x (add_CSNo y z) = add_CSNo (mul_CSNo x y) (mul_CSNo x z)