proposition: Lemma beval_merge_clause : forall env cl1 cl2, beval_clause env (Elim.merge_clause cl1 cl2) = (beval_clause env cl1 || beval_clause env cl2).
proof: Proof. unfold Elim.merge_clause. intros. destruct (Elim.split_clause cl1) as (cln1,clp1) eqn:SC1. destruct (Elim.split_clause cl2) as (cln2,clp2) eqn:SC2. rewrite! beval_clause_app. eapply beval_split_clause in SC1;eauto. eapply beval_split_clause in SC2;eauto. rewrite SC1. rewrite SC2. rewrite! beval_clause_app. btauto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause