proposition: Lemma wf_pset_mono : forall m m' (a: LitSet.t) (LE : hmap_order m m') (WF : wf_pset m a), wf_pset m' a.
proof: Proof. intros. destruct WF ; constructor ; auto. intros. apply wf_index0 in H. destruct H. destruct H. exists x; split; auto. eapply has_form_mono;eauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause