fix: type incorrect term produced by contradiction

This PR fixes a type error in the proof generated by the `contradiction` tactic.

closes #4851

src/Lean/Meta/Tactic/Contradiction.lean

@@ -160,7 +160,8 @@ def _root_.Lean.MVarId.contradictionCore (mvarId : MVarId) (config : Contradicti
         -- (h : ¬ p) (h' : p)
         if let some p ← matchNot? localDecl.type then
           if let some pFVarId ← findLocalDeclWithType? p then
-            mvarId.assign (← mkAbsurd (← mvarId.getType) (mkFVar pFVarId) localDecl.toExpr)
+            -- We use `False.elim` because `p`'s type may be Type
+            mvarId.assign (← mkFalseElim (← mvarId.getType) (mkApp localDecl.toExpr (mkFVar pFVarId)))
             return true
         -- (h : x ≠ x)
         if let some (_, lhs, rhs) ← matchNe? localDecl.type then

tests/lean/run/4851.lean

@@ -0,0 +1,2 @@
+theorem T0 (α : Type) (x : α) (H: α → False) : False := by
+  contradiction