proposition: Lemma wf_pset_empty : forall hm, wf_pset hm LitSet.empty.
proof: Proof. intros. constructor;auto. constructor. intros. unfold LitSet.mem in H. rewrite PTrie.gmem' in H. unfold LitSet.empty in H. rewrite empty_o in H. simpl in H. congruence. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause