proposition: Lemma wf_watch_clause_of_list : forall m l w (HF : Forall (has_literal m) l) (WC : watch_clause_of_list l = Some w), has_watched_clause m w.
proof: Proof. intros. unfold watch_clause_of_list in WC. destruct l; try congruence. destruct l0; try congruence. inv WC. unfold has_watched_clause. simpl. auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause