const Repl : set (set set) set const Inj1 : set set term Inj0 = \x:set.Repl x Inj1 const Empty : set axiom Repl_Empty: !f:set set.Repl Empty f = Empty claim Inj0 Empty = Empty