Description: Formula-building lemma for use with the Distinctor Reduction Theorem.
Proof revision is marked as discouraged because the minimizer replaces
albidv with dral2 , leading to a one byte longer proof. However
feel free to manually edit it according to conventions. (TODO: dral2 depends on ax-13 , hence its usage during minimizing is discouraged.
Check in the long run whether this is a permanent restriction). Usage
of this theorem is discouraged because it depends on ax-13 .
(Contributed by Mario Carneiro, 8-Oct-2016) Avoid ax-8 . (Revised by Wolf Lammen, 22-Sep-2024)(Proof modification is discouraged.)(New usage is discouraged.)