∀ (thm : Lean.Meta.Grind.EMatchTheorem) (proof prop : Lean.Expr) (generation : ℕ)
  (guards : List Lean.Meta.Grind.TheoremGuard) (thm_1 : Lean.Meta.Grind.EMatchTheorem) (proof_1 prop_1 : Lean.Expr)
  (generation_1 : ℕ) (guards_1 : List Lean.Meta.Grind.TheoremGuard),
  ({ thm := thm, proof := proof, prop := prop, generation := generation, guards := guards } =
      { thm := thm_1, proof := proof_1, prop := prop_1, generation := generation_1, guards := guards_1 }) =
    (thm = thm_1 ∧ proof = proof_1 ∧ prop = prop_1 ∧ generation = generation_1 ∧ guards = guards_1)