proposition: Lemma wf_pset_remove : forall hm i d, wf_pset hm d -> wf_pset hm (LitSet.remove i d).
proof: Proof. intros. destruct H ; constructor ; auto. apply PTrie.wf_remove'; auto. intros. apply wf_index0. unfold LitSet.mem, LitSet.remove in *. rewrite PTrie.gmem' in *. rewrite grspec in H by assumption. destruct (eqs i0 i). discriminate. auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause