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