proposition: Lemma wf_remove_watched_clause : forall i cl s (WF : wf_state s) (HAS : has_watched_clause (hconsmap s) cl), wf_state (remove_watched_clause i cl s).
proof: Proof. intros. intros. destruct WF ; constructor ; simpl ; auto. apply wf_remove_watched_id ; auto. apply WMap.wf_remove_watched_id ; auto. apply wf_remove_watched_id ; auto. apply WMap.wf_remove_watched_id ; auto. apply WMap.wf_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