proposition: Lemma eval_annot_extract_state : forall st l st', eval_annot_state st -> extract_unit st = Some (l,st') -> eval_annot eval_literal (hconsmap st) l /\ eval_annot_state st'.
proof: Proof. unfold extract_unit. intros. destruct (unit_stack st) eqn:EQ; try congruence. inv H0. destruct H. rewrite EQ in ev_an_stack0. unfold eval_stack in ev_an_stack0. inv ev_an_stack0. split ; auto. constructor; simpl ; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause