proposition: Lemma isMono_lift : forall {A:Type} (F : hmap -> A -> Prop), isMono F -> isMono (fun hm : hmap => Annot.lift (F hm)).
proof: Proof. unfold isMono ; intros. eapply H ; eauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause