Description: Lemma for founded recursion. The founded recursion generator's domain is a subclass of A . (Contributed by Scott Fenton, 27-Aug-2022)