const CSNo : set prop const SNo : set prop const CSNo_Re : set set axiom CSNo_ReR: !x:set.CSNo x -> SNo (CSNo_Re x) const mul_CSNo : set set set const ordsucc : set set const Empty : set lemma !x:set.CSNo x -> CSNo (mul_CSNo (ordsucc Empty) x) -> SNo (CSNo_Re x) -> mul_CSNo (ordsucc Empty) x = x var x:set hyp CSNo x claim CSNo (mul_CSNo (ordsucc Empty) x) -> mul_CSNo (ordsucc Empty) x = x