{P : Sort u} →
  {ref : Lean.Syntax} →
    {fvarId : Lean.FVarId} →
      {attrs : Array Lean.Elab.Attribute} →
        {shortDeclName declName : Lean.Name} →
          {parentName? : Option Lean.Name} →
            {lctx : Lean.LocalContext} →
              {localInstances : Lean.LocalInstances} →
                {type val : Lean.Expr} →
                  {mvarId : Lean.MVarId} →
                    {termination : Lean.Elab.TerminationHints} →
                      {binders : Lean.Syntax} →
                        {docString? : Option (Lean.TSyntax `Lean.Parser.Command.docComment × Bool)} →
                          {ref' : Lean.Syntax} →
                            {fvarId' : Lean.FVarId} →
                              {attrs' : Array Lean.Elab.Attribute} →
                                {shortDeclName' declName' : Lean.Name} →
                                  {parentName?' : Option Lean.Name} →
                                    {lctx' : Lean.LocalContext} →
                                      {localInstances' : Lean.LocalInstances} →
                                        {type' val' : Lean.Expr} →
                                          {mvarId' : Lean.MVarId} →
                                            {termination' : Lean.Elab.TerminationHints} →
                                              {binders' : Lean.Syntax} →
                                                {docString?' :
                                                    Option (Lean.TSyntax `Lean.Parser.Command.docComment × Bool)} →
                                                  { ref := ref, fvarId := fvarId, attrs := attrs,
                                                        shortDeclName := shortDeclName, declName := declName,
                                                        parentName? := parentName?, lctx := lctx,
                                                        localInstances := localInstances, type := type, val := val,
                                                        mvarId := mvarId, termination := termination,
                                                        binders := binders, docString? := docString? } =
                                                      { ref := ref', fvarId := fvarId', attrs := attrs',
                                                        shortDeclName := shortDeclName', declName := declName',
                                                        parentName? := parentName?', lctx := lctx',
                                                        localInstances := localInstances', type := type', val := val',
                                                        mvarId := mvarId', termination := termination',
                                                        binders := binders', docString? := docString?' } →
                                                    (ref = ref' →
                                                        fvarId = fvarId' →
                                                          attrs = attrs' →
                                                            shortDeclName = shortDeclName' →
                                                              declName = declName' →
                                                                parentName? = parentName?' →
                                                                  lctx = lctx' →
                                                                    localInstances = localInstances' →
                                                                      type = type' →
                                                                        val = val' →
                                                                          mvarId = mvarId' →
                                                                            termination = termination' →
                                                                              binders = binders' →
                                                                                docString? = docString?' → P) →
                                                      P