proposition: Lemma wf_remove_watched_id : forall l i cls (WF: wf cls) , wf (remove_watched_id l i cls).
proof: Proof. intros. rewrite remove_clause_eq by auto. apply wf_remove_watched_id_old; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause