const If_i : prop set set set term If_iii = \P:prop.\g:set set set.\h:set set set.\x:set.\y:set.If_i P (g x y) (h x y) 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.!g:set set set.!h:set set set.~ P -> If_iii P g h = h