proposition: Lemma eval_annot_reduce_lits : forall m u (WFU : wf_units_lit u m) (EV : eval_annot_units u m) cl (WFC : Forall (has_literal m) cl) an (WFA : wf_pset m an) (EC : eval_pset m an -> eval_literal_list cl), (ohold (eval_annot eval_literal_list m) (reduce_lits u an cl)).
proof: Proof. intros m u WFU EV cl WFC. induction WFC. - simpl in *. auto. - simpl in *. destruct (find_lit x u) eqn:EQ. assert (EQ':=EQ). apply eval_annot_units_find_lit with (m:=m) in EQ; auto. apply check_annot_find_lit with (hm:=m) in EQ'; auto. unfold eval_annot, Annot.map in EQ,EQ'. simpl in EQ,EQ'. + destruct (Annot.elt t0) ; simpl ; auto. intros. assert (WFUnion : wf_pset m (LitSet.union (Annot.deps t0) an)). { apply wf_pset_union;auto. } apply IHWFC; auto. intro. apply eval_pset_union in H0 ; auto. apply eval_neg_literal_rec in EC; auto. tauto. tauto. destruct EQ';auto. destruct WFA;auto. + intros. specialize (IHWFC an WFA). specialize (subset_reduce_lits u m WFU l an (wf_map_pset m _ WFA)). destruct (reduce_lits u an l) eqn:EQ1; simpl in *; auto. unfold Annot.map, eval_annot in *. simpl in *. intros (WFM & SUB). intro. eapply eval_pset_subset in SUB; eauto. destruct x ; simpl in *; auto. tauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause