{P : Sort u} →
  {type : Lean.Expr} →
    {structNameSet : Lean.NameSet} →
      {fieldMap : Lean.NameMap Lean.Expr} →
        {fields : Array Lean.Expr} →
          {instMVars : Array Lean.MVarId} →
            {liftedFVars : Array Lean.Expr} →
              {liftedFVarRemap : Lean.FVarIdMap Lean.FVarId} →
                {optParamFields : Array (Lean.Name × Lean.Expr × Bool)} →
                  {type' : Lean.Expr} →
                    {structNameSet' : Lean.NameSet} →
                      {fieldMap' : Lean.NameMap Lean.Expr} →
                        {fields' : Array Lean.Expr} →
                          {instMVars' : Array Lean.MVarId} →
                            {liftedFVars' : Array Lean.Expr} →
                              {liftedFVarRemap' : Lean.FVarIdMap Lean.FVarId} →
                                {optParamFields' : Array (Lean.Name × Lean.Expr × Bool)} →
                                  { type := type, structNameSet := structNameSet, fieldMap := fieldMap,
                                        fields := fields, instMVars := instMVars, liftedFVars := liftedFVars,
                                        liftedFVarRemap := liftedFVarRemap, optParamFields := optParamFields } =
                                      { type := type', structNameSet := structNameSet', fieldMap := fieldMap',
                                        fields := fields', instMVars := instMVars', liftedFVars := liftedFVars',
                                        liftedFVarRemap := liftedFVarRemap', optParamFields := optParamFields' } →
                                    (type = type' →
                                        structNameSet = structNameSet' →
                                          fieldMap = fieldMap' →
                                            fields = fields' →
                                              instMVars = instMVars' →
                                                liftedFVars = liftedFVars' →
                                                  liftedFVarRemap = liftedFVarRemap' →
                                                    optParamFields = optParamFields' → P) →
                                      P