proposition: Lemma IntMapForallAnd : forall {A: Type} (P1 P2: A -> Prop) l, IntMapForall P1 l -> IntMapForall P2 l -> IntMapForall (fun x => P1 x /\ P2 x) l.
proof: Proof. repeat intro. unfold IntMapForall in *. split ; eauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause