const If_i : prop set set set term If_ii = \P:prop.\f:set set.\f2:set set.\x:set.If_i P (f x) (f2 x) axiom If_i_0: !P:prop.!x:set.!y:set.~ P -> If_i P x y = y axiom func_ext: !f:set set.!f2:set set.(!x:set.f x = f2 x) -> f = f2 claim !P:prop.!f:set set.!f2:set set.~ P -> If_ii P f f2 = f2