term Descr_Vo1 = \P:(set prop) prop.\x:set.!p:set prop.P p -> p x var P:(set prop) prop var p:set prop hyp !q:set prop.!p2:set prop.P q -> P p2 -> q = p2 hyp P p claim p = Descr_Vo1 P -> P (Descr_Vo1 P)