const Inj0 : set set const Empty : set axiom Inj0_0: Inj0 Empty = Empty const setsum : set set set axiom Inj0_setsum_0L: !x:set.setsum Empty x = Inj0 x claim setsum Empty Empty = Empty