proposition: Lemma has_clauses_mono : isMono has_clauses.
proof: Proof. unfold has_clauses. apply WMap.Forall_mono; auto. apply check_annot_mono. apply isMono_lift. apply has_watched_clause_mono. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause