proposition: Lemma wf_map_remove_watched_id : forall l id cls (WF: wf_map cls), wf_map (remove_watched_id l id cls).
proof: Proof. unfold remove_watched_id. intros. destruct l. apply IntMap.wf_insert'; auto. constructor. apply IntMap.wf_insert'; auto. constructor. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause