const Eps_i : (set prop) set term Descr_ii = \P:(set set) prop.\x:set.Eps_i \y:set.!f:set set.P f -> f x = y var P:(set set) prop var f:set set hyp !f2:set set.!f3:set set.P f2 -> P f3 -> f2 = f3 hyp P f claim f = Descr_ii P -> P (Descr_ii P)