diff --git a/include/cvc5/cvc5_proof_rule.h b/include/cvc5/cvc5_proof_rule.h
index 0fc3531159f..cec7c58ca5b 100644
--- a/include/cvc5/cvc5_proof_rule.h
+++ b/include/cvc5/cvc5_proof_rule.h
@@ -2677,6 +2677,19 @@ enum ENUM(ProofRewriteRule)
    * \endverbatim
    */
   EVALUE(DT_CONS_EQ),
+  /**
+   * \verbatim embed:rst:leading-asterisk
+   * **Datatypes -- cycle**
+   *
+   * .. math::
+   *   (x = t[x]) = \bot
+   *
+   * where all terms on the path to :math:`x` in :math:`t[x]` are applications
+   * of constructors, and this path is non-empty.
+   *
+   * \endverbatim
+   */
+  EVALUE(DT_CYCLE),
   /**
    * \verbatim embed:rst:leading-asterisk
    * **Datatypes -- collapse tester**
diff --git a/src/api/cpp/cvc5_proof_rule_template.cpp b/src/api/cpp/cvc5_proof_rule_template.cpp
index 441b186e25d..359077bf12a 100644
--- a/src/api/cpp/cvc5_proof_rule_template.cpp
+++ b/src/api/cpp/cvc5_proof_rule_template.cpp
@@ -257,6 +257,7 @@ const char* toString(cvc5::ProofRewriteRule rule)
     case ProofRewriteRule::DT_COLLAPSE_TESTER_SINGLETON:
       return "dt-collapse-tester-singleton";
     case ProofRewriteRule::DT_CONS_EQ: return "dt-cons-eq";
+    case ProofRewriteRule::DT_CYCLE: return "dt-cycle";
     case ProofRewriteRule::DT_COLLAPSE_UPDATER: return "dt-collapse-updater";
     case ProofRewriteRule::DT_UPDATER_ELIM: return "dt-updater-elim";
     case ProofRewriteRule::DT_MATCH_ELIM: return "dt-match-elim";
diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp
index 2c500b85a00..b76c7088865 100644
--- a/src/theory/datatypes/datatypes_rewriter.cpp
+++ b/src/theory/datatypes/datatypes_rewriter.cpp
@@ -57,6 +57,8 @@ DatatypesRewriter::DatatypesRewriter(NodeManager* nm,
                            TheoryRewriteCtx::PRE_DSL);
   registerProofRewriteRule(ProofRewriteRule::DT_MATCH_ELIM,
                            TheoryRewriteCtx::PRE_DSL);
+  registerProofRewriteRule(ProofRewriteRule::DT_CYCLE,
+                           TheoryRewriteCtx::PRE_DSL);
 }
 
 Node DatatypesRewriter::rewriteViaRule(ProofRewriteRule id, const Node& n)
@@ -184,6 +186,34 @@ Node DatatypesRewriter::rewriteViaRule(ProofRewriteRule id, const Node& n)
       }
     }
     break;
+    case ProofRewriteRule::DT_CYCLE:
+    {
+      if (n.getKind() == Kind::EQUAL && n[0] != n[1])
+      {
+        std::unordered_set<TNode> visited;
+        std::vector<TNode> visit;
+        TNode cur;
+        visit.push_back(n[1]);
+        do
+        {
+          cur = visit.back();
+          visit.pop_back();
+          if (visited.find(cur) == visited.end())
+          {
+            visited.insert(cur);
+            if (cur == n[0])
+            {
+              return d_nm->mkConst(false);
+            }
+            if (cur.getKind() == Kind::APPLY_CONSTRUCTOR)
+            {
+              visit.insert(visit.end(), cur.begin(), cur.end());
+            }
+          }
+        } while (!visit.empty());
+      }
+    }
+    break;
     default: break;
   }
   return Node::null();
diff --git a/src/theory/datatypes/infer_proof_cons.cpp b/src/theory/datatypes/infer_proof_cons.cpp
index 16bc45bc25f..fe28933540b 100644
--- a/src/theory/datatypes/infer_proof_cons.cpp
+++ b/src/theory/datatypes/infer_proof_cons.cpp
@@ -317,9 +317,42 @@ void InferProofCons::convert(InferenceId infer, TNode conc, TNode exp, CDProof*
       }
     }
     break;
+    case InferenceId::DATATYPES_CYCLE:
+    {
+      Assert(!expv.empty());
+      Node lastEq = expv[expv.size() - 1];
+      Assert(lastEq.getKind() == Kind::EQUAL);
+      std::vector<Node> subs(expv.begin(), expv.begin() + expv.size() - 1);
+      ProofChecker* pc = d_env.getProofNodeManager()->getChecker();
+      Node eq;
+      if (!subs.empty())
+      {
+        eq = pc->checkDebug(ProofRule::SUBS, subs, {lastEq[1]});
+        Assert(!eq.isNull());
+        cdp->addStep(eq, ProofRule::SUBS, subs, {lastEq[1]});
+      }
+      else
+      {
+        eq = lastEq[1].eqNode(lastEq[1]);
+      }
+      Node eq1 = lastEq[0].eqNode(eq[1]);
+      Trace("dt-ipc-cycle") << "Cycle eq? " << eq1 << std::endl;
+      Node falsen =
+          d_env.getRewriter()->rewriteViaRule(ProofRewriteRule::DT_CYCLE, eq1);
+      if (!falsen.isNull())
+      {
+        Node eqq = eq1.eqNode(falsen);
+        cdp->addTheoryRewriteStep(eqq, ProofRewriteRule::DT_CYCLE);
+        cdp->addStep(falsen, ProofRule::EQ_RESOLVE, {eq1, eqq}, {});
+        if (eq1 != lastEq)
+        {
+          cdp->addStep(eq1, ProofRule::TRANS, {lastEq, eq}, {});
+        }
+      }
+    }
+    break;
     // inferences currently not supported
     case InferenceId::DATATYPES_BISIMILAR:
-    case InferenceId::DATATYPES_CYCLE:
     default:
       Trace("dt-ipc") << "...no conversion for inference " << infer
                       << std::endl;