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 var x:set hyp P f hyp !f2:set set.P f2 -> f2 x = f x claim (!f2:set set.P f2 -> f2 x = Descr_ii P x) -> f x = Descr_ii P x