proposition: Lemma wf_remove_lit : forall a s, LitSet.wf s -> LitSet.wf (remove_lit a s).
proof: Proof. unfold remove_lit. intros. unfold LitSet.remove. apply IntMap.wf_remove'; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause