proposition: Lemma forall_units_mono : forall m m' P u (OH: hmap_order m m') (WU: wf_units_lit u m) (EU: forall_units P m u), forall_units P m' u.
proof: Proof. unfold wf_units_lit. intros. unfold forall_units in *. intros. destruct H. assert (H':= H). apply WU in H. destruct H as (VI & WF). apply EU; auto. unfold units_has_literal. split ; auto. unfold Annot.lift. rewrite has_form_of_literal. destruct VI as (f1 & HF &EQ). assert (Annot.lift form_of_literal l = f1). { apply has_form_eq with (m:= m'); auto. unfold Annot.lift in *. apply has_form_of_literal ;auto. revert HF. apply has_form_mono; auto. } unfold Annot.lift in H. congruence. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause