proposition: Lemma resolve_all_eval : forall env lp ln, beval_cnf env (Elim.resolve_all lp ln)= true -> forall clp cln, In clp lp -> In cln ln -> beval_clause env clp = true \/ beval_clause env cln = true.
proof: Proof. induction lp;simpl. - tauto. - intros. rewrite beval_cnf_app in H. rewrite andb_true_iff in H. destruct H as [E1 E2]. destruct H0 ; subst. rewrite beval_cnf_normalise in E1. rewrite beval_cnf_merge_clause in E1. rewrite orb_true_iff in E1. destruct E1 ; auto. right. revert cln H1. rewrite <- Forall_forall. apply beval_cnf_Forall;auto. eapply IHlp;eauto. Qed.
imports: ZArith List Bool Lia Morphisms Cdcl.Syntax Cdcl.Lib Cdcl.Lit Cdcl.Clause