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) lemma !x:set.!y:set.CSNo x -> CSNo y -> CSNo (add_CSNo x y) -> CSNo (add_CSNo y x) -> add_CSNo x y = add_CSNo y x var x:set var y:set hyp CSNo x hyp CSNo y claim CSNo (add_CSNo x y) -> add_CSNo x y = add_CSNo y x