proposition: Lemma wf_pset_union : forall hm d d', wf_pset hm d -> wf_pset hm d' -> wf_pset hm (LitSet.union d d').
proof: Proof. intros. destruct H, H0 ; constructor ; auto. apply LitSet.wf_union; auto. intros. rewrite <- LitSet.mem_union in H by auto. intuition. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause