proposition: Lemma beval_cnf_merge_clause : forall env clp ln, beval_cnf env (map (Elim.merge_clause clp) ln) = beval_clause env clp || beval_cnf env ln.
proof: Proof. induction ln. - simpl. rewrite orb_comm. reflexivity. - simpl. rewrite IHln. rewrite beval_merge_clause. btauto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause