proposition: Lemma eval_insert_literal : forall l st (WF : wf_state st) (HF : check_annot has_literal (hconsmap st) l) (EV : eval_state st) (EL : Annot.lift eval_literal l), eval_state (insert_literal l st) /\ wf_state (insert_literal l st).
proof: Proof. split. - unfold insert_literal. destruct EV ; constructor ; simpl; auto. eapply eval_add_literal ; eauto. destruct WF ; auto. destruct HF ; auto. - apply wf_insert_literal ; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause