{P : Sort u} →
  {sz offset : ℕ} →
    {type : Lean.Expr} →
      {sz' offset' : ℕ} →
        {type' : Lean.Expr} →
          Lean.Compiler.LCNF.CtorFieldInfo.scalar sz offset type =
              Lean.Compiler.LCNF.CtorFieldInfo.scalar sz' offset' type' →
            (sz = sz' → offset = offset' → type = type' → P) → P