proposition: Lemma ForallAND : forall P Q cls, Forall P cls -> Forall Q cls -> Forall (fun cl : Annot.t watched_clause => P cl /\ Q cl) cls.
proof: Proof. intros. unfold Forall in *. specialize (IntMapForallAnd _ _ _ H H0). apply IntMapForall_Forall. intros. destruct H1. destruct H1. destruct H2. split. apply IntMapForallAnd ; auto. apply IntMapForallAnd ; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause