proposition: Lemma wf_augment_with_clause : forall cl st (HAS : has_conflict_clause (hconsmap st) cl) (WF: wf_state st), wf_result_state (augment_with_clause cl st).
proof: Proof. unfold augment_with_clause. intros. generalize (wf_get_fresh_clause_id st WF). generalize (hconsmap_get_fresh_clause_id st). destruct (get_fresh_clause_id st) as (fr,st'). simpl. intros. rewrite <- H in *. apply wf_insert_normalised_clause; auto. apply wf_make_clause;auto. destruct H0; auto. auto with wf. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause