list.update_same

Stream: Is there code for X?

[Marcus Rossel]

Is there something like: ?

lemma list.update_same {α : Type*} (l : list α) (n : ℕ) (a a' : α) :
  (l.update_nth n a).update_nth n a' = l.update_nth n a'

[Yakov Pechersky]

As always, induction is your friend:

lemma list.update_same {α : Type*} (l : list α) (n : ℕ) (a a' : α) :
  (l.update_nth n a).update_nth n a' = l.update_nth n a' :=
begin
  induction l with hd tl hl generalizing n,
  { simp [list.update_nth] },
  { cases n,
    { simp [list.update_nth] },
    { simp [list.update_nth, hl] } }
end