I have a recursive function that updates a map (string, bool).
I am trying to implement a predicate that ensures the last state of said map, however, dafny has some troubles trying to verify even the esiest postconditions.

This is my code:

    function updateMapRecursive(s: seq<(string, string, bool)>, m: map<string, bool>): (map<string, bool>, bool)
    decreases s
    ensures forall k :: k in m <==> k in updateMapRecursive(s, m).0
    ensures s==[] ==> updateMapRecursive(s, m) == (m, true)
    ensures (|s|>0 && !(s[0].0 in m && s[0].1 in m)) ==> updateMapRecursive(s, m) == (m, false)
    ensures (|s|>0 && (s[0].0 in m && s[0].1 in m)) ==> !m[s[0].0] ==> updateMapRecursive(s, m) == updateMapRecursive(s[1..], m)
    ensures (|s|>0 && (s[0].0 in m && s[0].1 in m)) ==> m[s[0].0] ==> updateMapRecursive(s, m) == updateMapRecursive(s[1..], m[s[0].1:=s[0].2])
    {
        if s==[] then (m, true)
        else
            if !(s[0].0 in m && s[0].1 in m) then (m, false)
            else
                if m[s[0].0] then
                    updateMapRecursive(s[1..], m[s[0].1:=s[0].2])
                else
                    updateMapRecursive(s[1..], m)
    }

    predicate map_after_updateRecusive(s: seq<(string, string, bool)>, m: map<string, bool>, m': map<string, bool>)
        ensures (m', true) == updateMapRecursive(s, m)
    {
        if s == [] then
            assert updateMapRecursive(s, m) == (m, true);
            assert m==m' <==> updateMapRecursive(s, m) == (m', true); //correctly verified
            m'==m
        else
            assume (m', true) == updateMapRecursive(s, m);
            true
    }

As you can see I haven’t yet implemented the recursive case in the predicate so I put an assume clause. Dafny verify correctly both asserts in the first ‘if’, however it can’t verify the postcondition in that return path, even though it is explicitly verified in the second assert.

¿Can anyone help me please?