proposition: Lemma insert_unit_correct : forall l st, wf_state st -> check_annot has_literal (hconsmap st) l -> wf_state (insert_unit l st) /\ hconsmap (insert_unit l st) = hconsmap st /\ (Annot.lift eval_literal l -> eval_state st -> eval_state (insert_unit l st)) /\ (eval_annot_state st -> eval_annot eval_literal (hconsmap st) l -> eval_annot_state (insert_unit l st)).
proof: Proof. intros. split_and. - apply wf_insert_unit; auto. - destruct st ; simpl; reflexivity. - intros. apply eval_insert_unit; auto. - intros. apply eval_annot_insert_unit; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause