proposition: Lemma augment_hyp_not_OutOfFuel : forall b a st, ~ is_fail (augment_hyp b a st).
proof: Proof. unfold augment_hyp. intros. unfold augment_cnf. destruct ( cnf_of_literal a b (fst (defs (insert_unit (annot_hyp a) st))) (snd (defs (insert_unit (annot_hyp a) st))) (arrows (insert_unit (annot_hyp a) st)) nil (elt (form_of_literal a)) (form_of_literal a)). destruct p. destruct p. apply fold_update_not_OutOfFuel. apply insert_fresh_watched_clause_not_OutOfFuel. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause