proposition: Lemma wf_remove_watched_id : forall m l i cls (WFW : WMap.wf cls) (WF : has_clauses m cls), has_clauses m (WMap.remove_watched_id l i cls).
proof: Proof. unfold has_clauses. intros. apply WMap.Forall_remove_watched_id; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause