proposition: Lemma has_watched_clause_mono : isMono has_watched_clause.
proof: Proof. unfold isMono. intros. unfold has_watched_clause in *. revert Fm. apply Forall_Forall. apply has_literal_mono;auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause