{P : Sort u_1} →
  {Functions : ℕ → Type u} →
    {Relations : ℕ → Type v} →
      {Functions' : ℕ → Type u} →
        {Relations' : ℕ → Type v} →
          { Functions := Functions, Relations := Relations } = { Functions := Functions', Relations := Relations' } →
            (Functions = Functions' → Relations = Relations' → P) → P