∀ (lctx₁ : Lean.LocalContext) (localInstances₁ : Lean.LocalInstances) (lctx₂ : Lean.LocalContext)
  (localInstances₂ : Lean.LocalInstances) (equalFVarIds : Std.HashMap Lean.FVarId Lean.FVarId)
  (lctx₁_1 : Lean.LocalContext) (localInstances₁_1 : Lean.LocalInstances) (lctx₂_1 : Lean.LocalContext)
  (localInstances₂_1 : Lean.LocalInstances) (equalFVarIds_1 : Std.HashMap Lean.FVarId Lean.FVarId),
  ({ lctx₁ := lctx₁, localInstances₁ := localInstances₁, lctx₂ := lctx₂, localInstances₂ := localInstances₂,
        equalFVarIds := equalFVarIds } =
      { lctx₁ := lctx₁_1, localInstances₁ := localInstances₁_1, lctx₂ := lctx₂_1, localInstances₂ := localInstances₂_1,
        equalFVarIds := equalFVarIds_1 }) =
    (lctx₁ = lctx₁_1 ∧
      localInstances₁ = localInstances₁_1 ∧
        lctx₂ = lctx₂_1 ∧ localInstances₂ = localInstances₂_1 ∧ equalFVarIds = equalFVarIds_1)