Description: A lemma for Conjunctive Normal Form unit propagation, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017) (Proof shortened by Wolf Lammen, 13-Apr-2024)