const Repl : set (set set) set const Power : set set const Empty : set const If_i : prop set set set const In : set set prop term iIn = In infix iIn 2000 2000 term UPair = \x:set.\y:set.Repl (Power (Power Empty)) \z:set.If_i (Empty iIn z) x y axiom If_i_or: !P:prop.!x:set.!y:set.If_i P x y = x | If_i P x y = y var x:set var y:set var z:set var w:set hyp w iIn Power (Power Empty) & x = If_i (Empty iIn w) y z claim x = If_i (Empty iIn w) y z -> x = y | x = z