proposition: Lemma not_fail_insert_watched_clause : forall diff i k st, ~ is_fail (insert_watched_clause diff i k st).
proof: Proof. unfold insert_watched_clause. intros. apply not_fail_insert_normalised_clause. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause