proposition: Lemma cat_dnfP e bcs1 bcs2 : qf_eval e (dnf_to_form (bcs1 ++ bcs2)) = qf_eval e (dnf_to_form bcs1 \/ dnf_to_form bcs2).
proof: Proof. by elim: bcs1 => //= bc1 bcs1 IH1; rewrite -orbA; congr orb; rewrite IH1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)