proposition: Lemma eval_annot_mono : forall {A:Type} (P: A -> Prop), isMono (eval_annot P).
proof: Proof. unfold isMono. intros. unfold eval_annot in *. intros. apply Fm. eapply eval_pset_mono; eauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause