proposition: Lemma eval_plus_or : forall l hf, elt hf = LOP LOR l -> Forall eval_watched_clause (List.map (fun fi : HFormula => {| watch1 := NEG fi; watch2 := POS hf; unwatched := nil |}) l).
proof: Proof. intros. rewrite Forall_forall. intros. rewrite in_map_iff in H0. destruct H0 as (f & (EQ & IN)). subst. unfold eval_watched_clause. simpl. intro. rewrite H. rewrite eval_formula_rew. left. simpl. rewrite eval_or_list_eq. rewrite eval_or_list'_Exists. rewrite Exists_exists. exists f ; split ; assumption. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause