proposition: Lemma cat_dnfP e bcs1 bcs2 : qf_eval e (odnf_to_oform (bcs1 ++ bcs2)) = qf_eval e (odnf_to_oform bcs1 \/ odnf_to_oform bcs2).
proof: Proof. by elim: bcs1 => //= bc1 bcs1 IH1; rewrite -orbA; congr orb; rewrite IH1. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq div choice fintype) mathcomp(bigop order ssralg finset fingroup zmodp) mathcomp(poly ssrnum)