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