∀ {I : Type u} {f : I → Type v} [inst : (i : I) → Sub (f i)] [inst_1 : DecidableEq I] (f₁ f₂ : (i : I) → f i) (i : I)
  (x₁ x₂ : f i), Function.update (f₁ - f₂) i (x₁ - x₂) = Function.update f₁ i x₁ - Function.update f₂ i x₂