proposition: Lemma eval_units_mono : forall m m' u (OH: hmap_order m m') (WU: wf_units_lit u m) (EU: eval_units m u), eval_units m' u.
proof: Proof. unfold eval_units. intros. eapply forall_units_mono; eauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause