proposition: Lemma eval_add_clause : forall l i wc cls (WF: WMap.wf cls) (EC: eval_clauses cls) (EW: Annot.lift eval_watched_clause wc), eval_clauses (WMap.add_clause l i wc cls).
proof: Proof. unfold eval_clauses. intros. apply WMap.Forall_add_clause; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause