proposition: Lemma forall_units_monoP : forall (P: hmap -> Annot.t literal -> Prop) m' m u (LE : hmap_order m' m) (PLE : forall l, P m' l -> P m l) (U : forall_units (P m') m u), forall_units (P m) m u.
proof: Proof. unfold forall_units. intros. apply U in H. apply PLE; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause