Description: Formula-building lemma for use with the Distinctor Reduction Theorem.
Part of Theorem 9.4 of Megill p. 448 (p. 16 of preprint). Usage of
this theorem is discouraged because it depends on ax-13 . Use the
weaker dral1v if possible. (Contributed by NM, 24-Nov-1994) Remove
dependency on ax-11 . (Revised by Wolf Lammen, 6-Sep-2018)(New usage is discouraged.)