proposition: Lemma check_annot_reduce : forall hm u l d x (WFU : wf_units_lit u hm) (HL : has_literal hm x) (HLL : Forall (has_literal hm) l) (WFD: wf_pset hm d), check_annot has_clause hm (reduce u d x l).
proof: Proof. induction l. - simpl. intros. constructor; simpl ; auto. - simpl. intros d x. destruct_in_goal SL. { intros. apply IHl;auto. inv HLL;auto. } destruct (find_lit a u) eqn:FL. intros. destruct (Annot.elt t0); auto. + apply check_annot_TRUE. + apply check_annot_find_lit with (hm:=hm) in FL; auto. inv HLL. apply IHl ; auto. apply wf_pset_union; auto. + intros. constructor;simpl; auto. inv HLL;auto. unfold Annot.lift. simpl. unfold has_watched_clause. constructor ; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause