proposition: Lemma hconsmap_augment_cnf : forall b a st, hconsmap_progress (augment_cnf b a) st.
proof: Proof. unfold augment_cnf. repeat intro. destruct (cnf_of_literal a b (fst (defs st)) (snd (defs st)) (arrows st) nil (elt (form_of_literal a)) (form_of_literal a)) as (((cp,cm),ar),acc). assert (HM := insert_defs_mono (cp,cm) ar st). revert H HM. generalize (insert_defs (cp, cm) ar st) as st'. intros. rewrite HM. clear. revert st'. induction acc; simpl; auto. intros. generalize (hconsmap_insert_fresh_watched_clause a st'). unfold hconsmap_progress. intro. specialize (H (insert_fresh_watched_clause_not_OutOfFuel a st')). destruct (insert_fresh_watched_clause a st'); simpl in *; auto. rewrite <- H. eapply IHacc;auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause