∀ {eNew impProof : Lean.Expr} {mvarIds : List Lean.MVarId} {eNew_1 impProof_1 : Lean.Expr}
  {mvarIds_1 : List Lean.MVarId},
  { eNew := eNew, impProof := impProof, mvarIds := mvarIds } =
      { eNew := eNew_1, impProof := impProof_1, mvarIds := mvarIds_1 } →
    eNew = eNew_1 ∧ impProof = impProof_1 ∧ mvarIds = mvarIds_1