proposition: Lemma ForallMono : forall {A: Type} (F: hmap -> A -> Prop) (M : isMono F), isMono (fun hm l => Forall (F hm) l).
proof: Proof. unfold isMono. intros. revert Fm. apply Forall_Forall. apply M; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause