const If_i : prop set set set axiom If_i_correct: !P:prop.!x:set.!y:set.P & If_i P x y = x | ~ P & If_i P x y = y claim !P:prop.!x:set.!y:set.~ P -> If_i P x y = y