Simplification in Conjunctive Normal Form

[nfbruns]

Hello,

I have been playing around with PyEDA and found out that in some cases further minimization could be done when converting to CNF. For Example: (~A|B)&A could also be stated as B&A. Because A has to be true, ~A has to be false and therefore can just be omitted from the clause.
For other cases like (A|B)&A PyEDA already does this kind of simplification.

Would be interested in your thoughts and thanks for this awesome Software!