const Unj : set set const Inj0 : set set axiom Unj_Inj0_eq: !x:set.Unj (Inj0 x) = x claim !x:set.!y:set.Inj0 x = Inj0 y -> x = y