diff --git a/library/Init/Lean/Level.lean b/library/Init/Lean/Level.lean
index b47d9bbe5a..f1c042294f 100644
--- a/library/Init/Lean/Level.lean
+++ b/library/Init/Lean/Level.lean
@@ -49,6 +49,11 @@ def isIMax : Level → Bool
 | imax _ _ => true
 | _        => false
 
+def isMaxIMax : Level → Bool
+| max _ _  => true
+| imax _ _ => true
+| _        => false
+
 def isParam : Level → Bool
 | param _ => true
 | _       => false
@@ -144,12 +149,6 @@ protected constant beq (a : @& Level) (b : @& Level) : Bool := default _
 
 instance : HasBeq Level := ⟨Level.beq⟩
 
-/- Return true if `a` and `b` denote the same level.
-   Check is currently incomplete.
-   TODO: implement in Lean. -/
-@[extern "lean_level_eqv"]
-constant isEquiv (a : @& Level) (b : @& Level) : Bool := default _
-
 /-- `occurs u l` return `true` iff `u` occurs in `l`. -/
 def occurs : Level → Level → Bool
 | u, l@(succ l₁)     => u == l || occurs u l₁
@@ -259,6 +258,12 @@ partial def normalize : Level → Level
         addOffset (mkIMaxAux l₁ l₂) k
     | _ => unreachable!
 
+
+/- Return true if `u` and `v` denote the same level.
+   Check is currently incomplete. -/
+def isEquiv (u v : Level) : Bool :=
+u == v || u.normalize == v.normalize
+
 /- Level to Format -/
 namespace LevelToFormat
 inductive Result