proposition: Lemma eval_pset_mono : forall m m' p, hmap_order m m' -> eval_pset m' p -> eval_pset m p.
proof: Proof. intros. unfold eval_pset in *. intros. apply H0 ; auto. eapply has_form_mono;eauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause