for x being set
for R being weakly-normalizing with_UN_property Relation st x is_a_normal_form_wrt R holds
nf (x,R) = x