proposition: Lemma check_annot_reduce_lits : forall m u cl (WFU: wf_units_lit u m) (WFC : Forall (has_literal m) cl) an (WFA : wf_pset m an) , ohold (check_annot has_conflict_clause m) (reduce_lits u an cl).
proof: Proof. intros m u cl WFU WFC. induction WFC ; simpl. - constructor. auto. constructor. - destruct (find_lit x u) eqn:FIND. + destruct (Annot.elt t0) ; simpl ; auto. intros. apply IHWFC. apply wf_pset_union;auto. apply check_annot_find_lit with (hm:=m) in FIND ;auto. + intros. specialize (IHWFC an WFA). destruct (reduce_lits u an l); simpl;auto. simpl in *. unfold Annot.lift, Annot.map in *. destruct IHWFC ; constructor ;auto. constructor;auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause