proposition: Lemma Forall_remove_watched_id : forall (P : Annot.t watched_clause -> Prop) l i cls (WF: wf cls) (ALL : Forall P cls), Forall P (remove_watched_id l i cls).
proof: Proof. intros. rewrite remove_clause_eq by auto. unfold remove_watched_id_old. intros. destruct (find_clauses_p (id_of_literal l) cls) eqn: FID. assert (FID':= FID). apply Forall_find_clauses with (P:=P) in FID. apply wf_find_clauses_p in FID'; auto. destruct FID, FID'. destruct (is_positive_literal l). apply IntMapForallAdd; auto. destruct WF ;auto. split ; simpl ; auto. apply IntMapForallRemove;auto. apply IntMapForallAdd; auto. destruct WF;auto. split ; simpl ; auto. apply IntMapForallRemove;auto. auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause