{P : Sort u} →
  {env : Lean.Environment} →
    {options : Lean.Options} →
      {currNamespace : Lean.Name} →
        {openDecls : List Lean.OpenDecl} →
          {env' : Lean.Environment} →
            {options' : Lean.Options} →
              {currNamespace' : Lean.Name} →
                {openDecls' : List Lean.OpenDecl} →
                  { env := env, options := options, currNamespace := currNamespace, openDecls := openDecls } =
                      { env := env', options := options', currNamespace := currNamespace', openDecls := openDecls' } →
                    (env = env' → options = options' → currNamespace = currNamespace' → openDecls = openDecls' → P) → P