-- Std.Http.Protocol.H1.Config
Std.Http.Protocol.H1.Config.mk.injEq : ∀ (maxMessages maxHeaders maxHeaderBytes : ℕ) (enableKeepAlive : Bool) (agentName : Option Std.Http.Header.Value)
  (maxUriLength maxStartLineLength maxHeaderNameLength maxHeaderValueLength maxSpaceSequence maxLeadingEmptyLines
    maxChunkExtensions maxChunkExtNameLength maxChunkExtValueLength maxChunkLineLength maxChunkSize maxBodySize
    maxReasonPhraseLength maxTrailerHeaders maxMessages_1 maxHeaders_1 maxHeaderBytes_1 : ℕ)
  (enableKeepAlive_1 : Bool) (agentName_1 : Option Std.Http.Header.Value)
  (maxUriLength_1 maxStartLineLength_1 maxHeaderNameLength_1 maxHeaderValueLength_1 maxSpaceSequence_1
    maxLeadingEmptyLines_1 maxChunkExtensions_1 maxChunkExtNameLength_1 maxChunkExtValueLength_1 maxChunkLineLength_1
    maxChunkSize_1 maxBodySize_1 maxReasonPhraseLength_1 maxTrailerHeaders_1 : ℕ),
  ({ maxMessages := maxMessages, maxHeaders := maxHeaders, maxHeaderBytes := maxHeaderBytes,
        enableKeepAlive := enableKeepAlive, agentName := agentName, maxUriLength := maxUriLength,
        maxStartLineLength := maxStartLineLength, maxHeaderNameLength := maxHeaderNameLength,
        maxHeaderValueLength := maxHeaderValueLength, maxSpaceSequence := maxSpaceSequence,
        maxLeadingEmptyLines := maxLeadingEmptyLines, maxChunkExtensions := maxChunkExtensions,
        maxChunkExtNameLength := maxChunkExtNameLength, maxChunkExtValueLength := maxChunkExtValueLength,
        maxChunkLineLength := maxChunkLineLength, maxChunkSize := maxChunkSize, maxBodySize := maxBodySize,
        maxReasonPhraseLength := maxReasonPhraseLength, maxTrailerHeaders := maxTrailerHeaders } =
      { maxMessages := maxMessages_1, maxHeaders := maxHeaders_1, maxHeaderBytes := maxHeaderBytes_1,
        enableKeepAlive := enableKeepAlive_1, agentName := agentName_1, maxUriLength := maxUriLength_1,
        maxStartLineLength := maxStartLineLength_1, maxHeaderNameLength := maxHeaderNameLength_1,
        maxHeaderValueLength := maxHeaderValueLength_1, maxSpaceSequence := maxSpaceSequence_1,
        maxLeadingEmptyLines := maxLeadingEmptyLines_1, maxChunkExtensions := maxChunkExtensions_1,
        maxChunkExtNameLength := maxChunkExtNameLength_1, maxChunkExtValueLength := maxChunkExtValueLength_1,
        maxChunkLineLength := maxChunkLineLength_1, maxChunkSize := maxChunkSize_1, maxBodySize := maxBodySize_1,
        maxReasonPhraseLength := maxReasonPhraseLength_1, maxTrailerHeaders := maxTrailerHeaders_1 }) =
    (maxMessages = maxMessages_1 ∧
      maxHeaders = maxHeaders_1 ∧
        maxHeaderBytes = maxHeaderBytes_1 ∧
          enableKeepAlive = enableKeepAlive_1 ∧
            agentName = agentName_1 ∧
              maxUriLength = maxUriLength_1 ∧
                maxStartLineLength = maxStartLineLength_1 ∧
                  maxHeaderNameLength = maxHeaderNameLength_1 ∧
                    maxHeaderValueLength = maxHeaderValueLength_1 ∧
                      maxSpaceSequence = maxSpaceSequence_1 ∧
                        maxLeadingEmptyLines = maxLeadingEmptyLines_1 ∧
                          maxChunkExtensions = maxChunkExtensions_1 ∧
                            maxChunkExtNameLength = maxChunkExtNameLength_1 ∧
                              maxChunkExtValueLength = maxChunkExtValueLength_1 ∧
                                maxChunkLineLength = maxChunkLineLength_1 ∧
                                  maxChunkSize = maxChunkSize_1 ∧
                                    maxBodySize = maxBodySize_1 ∧
                                      maxReasonPhraseLength = maxReasonPhraseLength_1 ∧
                                        maxTrailerHeaders = maxTrailerHeaders_1)