Description: Lemma for founded recursion. An acceptable function's domain is a subset of A . (Contributed by Paul Chapman, 21-Apr-2012)