chore: restore #4006 (#4038)

src/library/constructions/projection.cpp

@@ -99,10 +99,7 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
         expr proj_val  = mk_proj(n, i, c);
         proj_val = lctx.mk_lambda(proj_args, proj_val);
         declaration new_d;
-        // TODO: replace `if (false) {` with `if (is_prop) {`.
-        // Mathlib is crashing when prop fields are theorems.
-        // The crash is in the ir_interpreter. Kyle suspects this is an use-after-free bug in the interpreter.
-        if (false) { // if (is_prop) {
+        if (is_prop) {
             bool unsafe = use_unsafe(env, proj_type) || use_unsafe(env, proj_val);
             if (unsafe) {
                 // theorems cannot be unsafe

tests/lean/run/2575.lean

@@ -4,9 +4,8 @@ structure AtLeastThirtySeven where
 
 theorem AtLeastThirtySeven.lt (x : AtLeastThirtySeven) : 36 < x.val := x.le
 
--- TODO: fix
 /--
-info: def AtLeastThirtySeven.le : ∀ (self : AtLeastThirtySeven), 37 ≤ self.val :=
+info: theorem AtLeastThirtySeven.le : ∀ (self : AtLeastThirtySeven), 37 ≤ self.val :=
 fun self => self.2
 -/
 #guard_msgs in