proposition: Lemma wf_extract_unit : forall st l st', wf_state st -> extract_unit st = Some (l, st') -> wf_state st' /\ check_annot has_literal (hconsmap st') l.
proof: Proof. intros. unfold extract_unit in H0. destruct H. destruct (unit_stack st) eqn:EQ; try discriminate. inv H0. inv wf_stack0. split ; auto. constructor ; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause