Verify sequence of map modifications in dafny

I'm writing a function in dafny to verify a series of updates in a map in an iterative method, however, dafny cannot prove those changes in the map.

This is the code:

function updateMap(t: (bool, string, int), m: map<string, int>): map<string, int>
  requires t.1 in m
  ensures forall k :: k in m <==> k in updateMap(t, m)
  ensures t.0 ==> updateMap(t, m)[t.1] == t.2
{
  if t.0 then m[t.1:=t.2] else m
}

method updateMapIterative(s: seq<(bool, string, int)>, m: map<string, int>) returns (r: map<string, int>)
  requires forall t: (bool, string, int) :: t in s ==> t.1 in m
  ensures forall k :: k in m <==> k in r
  ensures forall t: (bool, string, int) :: t in s && t.0 ==> r[t.1] == t.2 //Can't prove this
{

  r := m;
  var i := 0;

  while i < |s|
    decreases |s|-i
    invariant 0 <= i <= |s|
    invariant forall t: (bool, string, int) :: t in s[0..i] ==> t.1 in r
    invariant forall k :: k in m <==> k in r
    invariant forall t: (bool, string, int) :: t in s[0..i] && t.0 ==> r[t.1] == t.2 //Can't prove this invariant
  {
    assert s[i].1 in m;
    r:= updateMap(s[i], m);
    assert s[i].0 ==> r[s[i].1] == s[i].2;
    i := i + 1;
    assert s[i-1].1 in m;
    assert s[i-1].0 ==> r[s[i-1].1] == s[i-1].2;
  }
}

But dafny cannot prove last invariant and I don't know how solve it (all the asserts are proved correctly but yet dafny can't solve the invariant). Can someone help me? Thank you!

You needed to specify if the same key existed anywhere in s otherwise you could be overwriting an earlier value. Also in Dafny maps are immutable object so you can't update m, but you can reassign r to a new value.

predicate distinct(s: seq<(bool, string, int)>) {
    forall x,y :: x != y && 0 <= x <= y < |s| ==> s[x].1 != s[y].1
}

method updateMapIterative(s: seq<(bool, string, int)>, m: map<string, int>) returns (r: map<string, int>)
  requires forall t: (bool, string, int) :: t in s ==> t.1 in m
  requires distinct(s)
  ensures forall k :: k in m <==> k in r
  ensures forall t: (bool, string, int) :: t in s && t.0 ==> r[t.1] == t.2 
{

  r := m;
  var i := 0;

  while i < |s|
    decreases |s|-i
    invariant 0 <= i <= |s|
    invariant forall t: (bool, string, int) :: t in s[0..i] ==> t.1 in r
    invariant forall k :: k in m <==> k in r
    invariant forall t: (bool, string, int) :: t in s[0..i] && t.0 ==> r[t.1] == t.2
  {
    assert s[i].1 in r;
    r:= updateMap(s[i], r); //assumed that you meant r instead of m
    i := i + 1;
  }
}