proposition: Lemma eval_remove_watched_clause : forall i cl st (ES: eval_state st) (WS: wf_state st) (EW : eval_watched_clause cl), eval_state (remove_watched_clause i cl st).
proof: Proof. unfold remove_watched_clause. intros. destruct ES ; destruct WS; constructor ; simpl ; auto. eapply eval_remove_watched_id;eauto. apply WMap.wf_remove_watched_id;auto. eapply eval_remove_watched_id;eauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause