proposition: Lemma wf_units_lit_mono : forall {A:Type}(u: IntMap.ptrie (Annot.t A)) m m', hmap_order m m' -> wf_units_lit u m -> wf_units_lit u m'.
proof: Proof. unfold wf_units_lit. intros. apply H0 in H1. destruct H1 ; split ; auto with wf. eapply valid_index_mono ; eauto. eapply wf_pset_mono;eauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause