diff --git a/src/Lean/Meta/SizeOf.lean b/src/Lean/Meta/SizeOf.lean
index 3eeb21b77c..3baab742c2 100644
--- a/src/Lean/Meta/SizeOf.lean
+++ b/src/Lean/Meta/SizeOf.lean
@@ -163,10 +163,14 @@ def mkSizeOfSpecLemmaName (ctorName : Name) : Name :=
 
 def mkSizeOfSpecLemmaInstance (ctorApp : Expr) : MetaM Expr :=
   matchConstCtor ctorApp.getAppFn (fun _ => throwError! "failed to apply 'sizeOf' spec, constructor expected{indentExpr ctorApp}") fun ctorInfo ctorLevels => do
+    let ctorArgs     := ctorApp.getAppArgs
+    let ctorFields   := ctorArgs[ctorArgs.size - ctorInfo.numFields:]
     let lemmaName  := mkSizeOfSpecLemmaName ctorInfo.name
-    let ctorArgs   := ctorApp.getAppArgs
-    let ctorFields := ctorArgs[ctorArgs.size - ctorInfo.numFields:]
-    mkAppM lemmaName ctorFields
+    let lemmaInfo  ← getConstInfo lemmaName
+    let lemmaArity ← forallTelescopeReducing lemmaInfo.type fun xs _ => return xs.size
+    let lemmaArgMask := mkArray (lemmaArity - ctorInfo.numFields) (none (α := Expr))
+    let lemmaArgMask := lemmaArgMask ++ ctorFields.toArray.map some
+    mkAppOptM lemmaName lemmaArgMask
 
 /- SizeOf spec theorem for nested inductive types -/
 namespace SizeOfSpecNested