proposition: Lemma eval_watched_clause_of_list : forall l w, eval_literal_list l -> watch_clause_of_list l = Some w -> eval_watched_clause w.
proof: Proof. unfold watch_clause_of_list. destruct l; try congruence. destruct l0; try congruence. intros. inv H0. unfold eval_watched_clause. simpl in *; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause