∀ {argMap : Lean.PHashMap (Lean.Expr × ℕ) (List (Lean.Expr × Lean.Expr))}
  {canon proofCanon : Lean.PHashMap Lean.Expr Lean.Expr}
  {canonArg : Lean.PHashMap Lean.Meta.Grind.CanonArgKey Lean.Expr}
  {argMap_1 : Lean.PHashMap (Lean.Expr × ℕ) (List (Lean.Expr × Lean.Expr))}
  {canon_1 proofCanon_1 : Lean.PHashMap Lean.Expr Lean.Expr}
  {canonArg_1 : Lean.PHashMap Lean.Meta.Grind.CanonArgKey Lean.Expr},
  { argMap := argMap, canon := canon, proofCanon := proofCanon, canonArg := canonArg } =
      { argMap := argMap_1, canon := canon_1, proofCanon := proofCanon_1, canonArg := canonArg_1 } →
    argMap = argMap_1 ∧ canon = canon_1 ∧ proofCanon = proofCanon_1 ∧ canonArg = canonArg_1