Description: Lemma for founded recursion. An acceptable function is a function. (Contributed by Paul Chapman, 21-Apr-2012)