proposition: Lemma wf_units_def_mono : forall {A: Type} m m' (w: @IntMap.ptrie int A) (LE : hmap_order m m') (WF : wf_units_def w m), wf_units_def w m'.
proof: Proof. unfold wf_units_def. intros. apply WF in H ; auto. destruct H as (f & FORM & ID). exists f ; split ; auto. revert FORM. apply has_form_mono;auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause