proposition: Lemma wf_remove_wneg : forall w l hm (WFM : wf_map w) (WF: wf_units_def w hm), wf_units_def (remove_wneg l w) hm.
proof: Proof. unfold wf_units_def, remove_wneg. intros. rewrite grspec in H by assumption. destruct (eqs i (id_of_literal l)). congruence. apply WF ; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause