proposition: Lemma has_conflict_clause_mono : isMono has_conflict_clause.
proof: Proof. unfold has_conflict_clause. intros m m' cl LE. apply Forall_Forall. intro. 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