proposition: Lemma wf_augment_hyp : forall b l st (HL: has_literal (hconsmap st) l) (WF: wf_state st), wf_result_state (augment_hyp b l st).
proof: Proof. unfold augment_hyp. intros. apply wf_augment_cnf; auto. apply wf_insert_unit ; auto. apply check_annot_hyp; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause