diff --git a/DocGen4/Process/DefinitionInfo.lean b/DocGen4/Process/DefinitionInfo.lean
index 6f709c1..ac4c90a 100644
--- a/DocGen4/Process/DefinitionInfo.lean
+++ b/DocGen4/Process/DefinitionInfo.lean
@@ -19,6 +19,14 @@ partial def stripArgs (e : Expr) : Expr :=
     stripArgs (Expr.instantiate1 body (mkFVar ⟨name⟩))
   | _ => e
 
+def valueToEq (v : DefinitionVal) : MetaM Expr := withLCtx {} {} do
+  withOptions (tactic.hygienic.set . false) do
+    lambdaTelescope v.value fun xs body => do
+      let us := v.levelParams.map mkLevelParam
+      let type ← mkEq (mkAppN (Lean.mkConst v.name us) xs) body
+      let type ← mkForallFVars xs type
+      return type
+
 def processEq (eq : Name) : MetaM CodeWithInfos := do
   let type ← (mkConstWithFreshMVarLevels eq >>= inferType)
   let final := stripArgs type
@@ -30,14 +38,25 @@ def DefinitionInfo.ofDefinitionVal (v : DefinitionVal) : MetaM DefinitionInfo :=
   let isNonComputable := isNoncomputable (← getEnv) v.name
   try
     let eqs? ← getEqnsFor? v.name
-    let equations ← eqs?.mapM (·.mapM processEq)
-    return {
-      toInfo := info,
-      isUnsafe,
-      hints := v.hints,
-      equations,
-      isNonComputable
-    }
+    match eqs? with
+    | some eqs =>
+      let equations ← eqs.mapM processEq
+      return {
+        toInfo := info,
+        isUnsafe,
+        hints := v.hints,
+        equations,
+        isNonComputable
+      }
+    | none =>
+      let equations := #[← prettyPrintTerm <| stripArgs (← valueToEq v)]
+      return {
+        toInfo := info,
+        isUnsafe,
+        hints := v.hints,
+        equations,
+        isNonComputable
+      }
   catch err =>
     IO.println s!"WARNING: Failed to calculate equational lemmata for {v.name}: {← err.toMessageData.toString}"
     return {