const Eps_i : (set prop) set term Descr_iii = \P:(set set set) prop.\x:set.\y:set.Eps_i \z:set.!g:set set set.P g -> g x y = z var P:(set set set) prop var g:set set set var x:set var y:set hyp P g hyp !h:set set set.P h -> h x y = g x y claim (!h:set set set.P h -> h x y = Descr_iii P x y) -> g x y = Descr_iii P x y