∀ {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} {𝓕 : Filter ι} (x x_1 : (i : ι) → R i) (e_x : x = x_1)
  (hx : ∀ᶠ (i : ι) in 𝓕, x i ∈ A i), RestrictedProduct.mk x hx = RestrictedProduct.mk x_1 ⋯