diff --git a/src/kernel/inductive.h b/src/kernel/inductive.h
index 27feac701d..dd6b2671b2 100644
--- a/src/kernel/inductive.h
+++ b/src/kernel/inductive.h
@@ -67,6 +67,8 @@ inline expr to_cnstr_when_structure(environment const & env, name const & induct
     expr e_type = whnf(infer_type(e));
     if (!is_constant(get_app_fn(e_type), induct_name))
         return e;
+    if (whnf(infer_type(e_type)) == mk_Prop())
+        return e;
     return expand_eta_struct(env, e_type, e);
 }