proposition: Lemma insert_fresh_watched_clause_not_OutOfFuel : forall a st, ~ is_fail (insert_fresh_watched_clause a st).
proof: Proof. unfold insert_fresh_watched_clause. intros. destruct_in_goal H. eapply not_fail_insert_watched_clause. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause