const Unj : set set const Inj1 : set set axiom Unj_Inj1_eq: !x:set.Unj (Inj1 x) = x claim !x:set.!y:set.Inj1 x = Inj1 y -> x = y