const If_i : prop set set set axiom If_i_1: !P:prop.!x:set.!y:set.P -> If_i P x y = x axiom If_i_0: !P:prop.!x:set.!y:set.~ P -> If_i P x y = y axiom xm: !P:prop.P | ~ P claim !P:prop.!x:set.!y:set.If_i P x y = x | If_i P x y = y