proposition: Lemma has_clause_reduce : forall m u w cl an (HASL : has_literal m w) (HASL : Forall (has_literal m) cl), Annot.lift (has_clause m) (reduce u an w cl).
proof: Proof. induction cl; simpl. - auto. - intros. inv HASL0. destruct_in_goal SL. auto. destruct (find_lit a u). destruct (Annot.elt t0) ; auto. + unfold Annot.lift. simpl ; auto. + simpl. unfold Annot.lift. simpl. unfold has_watched_clause ; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause