{P : Sort u} →
  {env : Lean.Environment} →
    {modName : Lean.Name} →
      {jpMap : Lean.IR.JPParamsMap} →
        {mainFn : Lean.IR.FunId} →
          {mainParams : Array Lean.IR.Param} →
            {env' : Lean.Environment} →
              {modName' : Lean.Name} →
                {jpMap' : Lean.IR.JPParamsMap} →
                  {mainFn' : Lean.IR.FunId} →
                    {mainParams' : Array Lean.IR.Param} →
                      { env := env, modName := modName, jpMap := jpMap, mainFn := mainFn, mainParams := mainParams } =
                          { env := env', modName := modName', jpMap := jpMap', mainFn := mainFn',
                            mainParams := mainParams' } →
                        (env = env' →
                            modName = modName' → jpMap = jpMap' → mainFn = mainFn' → mainParams = mainParams' → P) →
                          P