proposition: Lemma wf_add_clause : forall m l i wc cls (WFW : WMap.wf cls) (WF : has_clauses m cls) (WCL : check_annot has_watched_clause m wc), has_clauses m (WMap.add_clause l i wc cls).
proof: Proof. unfold has_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