proposition: Lemma wf_insert_literal : forall l st (WF : wf_state st) (HF : check_annot has_literal (hconsmap st) l), wf_state (insert_literal l st).
proof: Proof. intros. destruct WF ; constructor ; simpl ; auto with wf. { destruct (is_neg_arrow (Annot.elt l)). destruct HF; constructor ; auto. auto. } - unfold remove_wneg. auto with wf. - apply wf_remove_wneg; auto. - unfold add_literal. unfold wf_units_lit. intros. rewrite gsspec in H;auto. destruct (eqs i (id_of_literal (Annot.elt l)) ); auto. inv H. split. exists (form_of_literal (Annot.elt l)). split. apply has_form_of_literal; auto. destruct HF ; auto. auto. destruct HF ; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause