proposition: Lemma eval_annot_augment_clauses : forall prf st (WF : wf_state st) (WPA : Forall (has_conflict_clause (hconsmap st)) prf) (EP : Forall eval_literal_list prf) , eval_annot_state st -> eval_annot_result_state (augment_clauses prf st).
proof: Proof. unfold augment_clauses. induction prf; simpl; auto. - intros. inv EP. inv WPA. generalize (eval_annot_augment_with_clause a st WF H4 H H2). generalize (wf_augment_with_clause a st H4 WF). generalize (hconsmap_augment_with_clause a st). unfold hconsmap_progress. destruct (augment_with_clause a st) ; simpl; auto. intros. eapply IHprf;eauto. + revert H5. apply ForallMono. apply has_conflict_clause_mono. rewrite H0 by auto. auto with wf. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause