feat: abstract proofs in all declaration types

(draft)

Todo:
* perf measurements
* figure out unknown constant error in `tests/lean/magical.lean`

src/Lean/Elab/PreDefinition/Basic.lean

@@ -88,11 +88,15 @@ def applyAttributesOf (preDefs : Array PreDefinition) (applicationTime : Attribu
     applyAttributesAt preDef.declName preDef.modifiers.attrs applicationTime
 
 def abstractNestedProofs (preDef : PreDefinition) : MetaM PreDefinition := withRef preDef.ref do
-  if preDef.kind.isTheorem || preDef.kind.isExample then
+  if preDef.kind.isExample then
     pure preDef
-  else do
-    let value ← Meta.abstractNestedProofs preDef.declName preDef.value
-    pure { preDef with value := value }
+  else
+    let type ← Meta.abstractNestedProofs preDef.declName preDef.type
+    if preDef.kind.isTheorem then
+      pure { preDef with type }
+    else
+      let value ← Meta.abstractNestedProofs preDef.declName preDef.value
+      pure { preDef with type, value }
 
 /-- Auxiliary method for (temporarily) adding pre definition as an axiom -/
 def addAsAxiom (preDef : PreDefinition) : MetaM Unit := do

tests/lean/magical.lean.expected.out

@@ -6,3 +6,4 @@ but the projected value is not, it has type
   Nat
 magical.lean:5:8-5:18: error: (kernel) invalid projection
   h.2
+magical.lean:5:8-5:18: error: (kernel) unknown constant 'witness_eq.proof_1'