proposition: Lemma eval_reduce_lits : forall m u (EV : eval_units m u) cl (WFC : Forall (has_literal m) cl) an (EC : eval_literal_list cl), ohold (Annot.lift eval_literal_list) (reduce_lits u an cl).
proof: Proof. intros m u EV cl WFC. induction WFC. - simpl in *. auto. - simpl in *. destruct (find_lit x u) eqn:EQ. apply eval_units_find_lit with (m:=m) in EQ; auto. destruct (Annot.elt t0) ; simpl ; auto. intros. apply eval_neg_literal_rec in EC; auto. intros. generalize (IHWFC an). destruct (reduce_lits u an l); simpl in * ; auto. unfold Annot.map, Annot.lift. simpl. destruct x ; simpl in *. + tauto. + tauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause