diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean
index 335c432cdf..ee8e0738b2 100644
--- a/src/Lean/Elab/Match.lean
+++ b/src/Lean/Elab/Match.lean
@@ -477,19 +477,7 @@ partial def normalize (e : Expr) : M Expr := do
           normalize eNew
         else
           matchConstCtor e.getAppFn
-            (fun _ => do
-              if (← isProof e) then
-                /- We mark nested proofs as inaccessible. This is fine due to proof irrelevance.
-                   We need this feature to be able to elaborate definitions such as:
-                   ```
-                    def f : Fin 2 → Nat
-                      | 0 => 5
-                      | 1 => 45
-                   ```
-                -/
-                return mkInaccessible (← eraseInaccessibleAnnotations (← instantiateMVars e))
-              else
-                throwInvalidPattern e)
+            (fun _ => return mkInaccessible (← eraseInaccessibleAnnotations (← instantiateMVars e)))
             (fun v us => do
               let args := e.getAppArgs
               unless args.size == v.numParams + v.numFields do
diff --git a/tests/lean/run/finDotCtor.lean b/tests/lean/run/finDotCtor.lean
new file mode 100644
index 0000000000..a5f10ddfdb
--- /dev/null
+++ b/tests/lean/run/finDotCtor.lean
@@ -0,0 +1,16 @@
+def get : (as : List α) → (i : Fin as.length) → α
+  | a::as, .mk 0 _     => a
+  | a::as, .mk (i+1) h => get as (.mk i (Nat.lt_of_succ_lt_succ h))
+
+namespace Ex
+
+inductive Fin : Nat → Type
+  | zero : Fin (.succ n)
+  | succ : Fin n → Fin (.succ n)
+  deriving Repr
+
+def get : (as : List α) → (i : Fin as.length) → α
+  | a::as, .zero   => a
+  | a::as, .succ i => get as i
+
+end Ex