proposition: Lemma wf_add_wneg_lit : forall l wn hm (WFM : wf_map wn) (WF: wf_units_def wn hm) (HL : has_literal hm l), wf_units_def (add_wneg_lit l wn) hm.
proof: Proof. unfold add_wneg_lit. intros. destruct l ; auto. unfold wf_units_def in *. intros. rewrite gsspec in H; auto. destruct (eqs i (id f)) ; auto. simpl in HL. exists f ; simpl ; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause