(motive : Std.Http.Chunk.ExtensionName → Std.Http.Chunk.ExtensionName → Sort u_1) →
  (x x_1 : Std.Http.Chunk.ExtensionName) →
    ((a : String) →
        (a_1 : Std.Http.Chunk.IsValidExtensionName a) →
          (b : String) →
            (b_1 : Std.Http.Chunk.IsValidExtensionName b) →
              motive { value := a, isValidExtensionName := a_1 } { value := b, isValidExtensionName := b_1 }) →
      motive x x_1