Description: Lemma for well-founded recursion. For the next several theorems we will
be aiming to prove that dom F = A . To do this, we set up a
function C that supposedly contains an element of A that is not
in dom F and we show that the element must be in dom F . Our
choice of what to restrict F to depends on if we assume partial
orders or the axiom of infinity. To begin with, we establish the
functionality of C . (Contributed by Scott Fenton, 7-Dec-2022)