∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {n : ℕ} {xs : Vector α n} {a b c : α},
  (xs.push a).replace b c = if b ∈ xs then (xs.replace b c).push a else xs.push (if (b == a) = true then c else a)