proposition: Lemma check_annot_select_clause : forall b m u k v (WU : wf_units_lit u m) (CHK : check_annot has_watched_clause m v), ohold (check_annot has_conflict_clause m) (select_clause b u k v).
proof: Proof. unfold select_clause. intros. destruct CHK. destruct_in_goal R. rewrite lazy_or_orb. destruct_in_goal B. rewrite <- R. apply check_annot_reduce_lits; auto. simpl. auto. simpl. auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause