∀ {numClauses maxLit numClauses_1 maxLit_1 : ℕ},
  { numClauses := numClauses, maxLit := maxLit } = { numClauses := numClauses_1, maxLit := maxLit_1 } →
    numClauses = numClauses_1 ∧ maxLit = maxLit_1