proposition: Lemma wf_remove_watched_id_old : forall l i cls (WF: wf cls) , wf (remove_watched_id_old l i cls).
proof: Proof. unfold remove_watched_id_old. intros. destruct (find_clauses_p (id_of_literal l) cls) eqn:FD. apply wf_find_clauses_p in FD; auto. destruct FD. destruct (is_positive_literal l). apply wf_set ; auto. destruct WF;auto. apply IntMap.wf_remove';auto. apply wf_set ; auto. destruct WF;auto. apply IntMap.wf_remove';auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause