diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 6a5e887b82..413e5eda21 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -272,7 +272,6 @@ theorem heqOfEqRecEq {α β : Sort u} {a : α} {b : β} (h₁ : α = β) (h₂ :
   subst h₁
   apply heqOfEq
   exact h₂
-  done
 
 theorem castHEq {α β : Sort u} : (h : α = β) → (a : α) → cast h a ≅ a
   | rfl, a => HEq.refl a