proposition: Lemma Forall_mono : forall (F:hmap -> Annot.t watched_clause -> Prop) (Mono: isMono F) , isMono (fun m => Forall (F m) ).
proof: Proof. unfold WMap.Forall. intros. unfold isMono. intros m m' ORD x. set (G := fun m => IntMapForall2 (F m)). change (IntMapForall (G m) x -> IntMapForall (G m')x). apply IntMapForall_mono; auto. unfold G. intro. unfold IntMapForall2. intros. destruct H. split. revert H. apply IntMapForall_mono; auto. apply Mono; auto. revert H0. apply IntMapForall_mono; auto. apply Mono; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause