proposition: Lemma wf_cnf_hyps : forall b l st (HL: Forall (has_literal (hconsmap st)) l) (WF: wf_state st), wf_result_state (cnf_hyps b l st).
proof: Proof. unfold cnf_hyps. intros *. intro. change (Forall ((fun s => (has_literal (hconsmap s))) st) l) in HL. revert HL. apply fold_update_correct. - intros. revert H0. apply has_literal_mono. generalize (hconsmap_augment_hyp b a st0). unfold hconsmap_progress. rewrite H. simpl. intuition congruence. - intros. apply wf_augment_hyp; auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause