proposition: Lemma not_fail_update_watched_clause : forall d i cl st, ~ is_fail (update_watched_clause d i cl (Progress st)).
proof: Proof. unfold update_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