Gobra cannot prove preserves of empty function when indexing via two maps

[ThomasMayerl]

Assuming the following definitions:

type Foo struct {
    Bar int
}

var globalCache = map[string][]string{}
var globalFooCache = map[string]*Foo{}

In the following function, Gobra cannot automatically infer injectivity through the precondition:

preserves acc(globalCache)
preserves acc(globalFooCache)
preserves (forall str string :: str in globalCache ==> (
    let elems, _ := globalCache[str] in (
        forall k int :: 0 <= k && k < len(elems) ==> (acc(&elems[k]) &&
        acc(globalFooCache[elems[k]])))))
func test_map_slice_injective() {
}

If we explicitly assert injectivity in the preserves clause, Gobra cannot prove the postcondition, even though the function does not do anything:

preserves acc(globalCache)
preserves acc(globalFooCache)
preserves (forall str string :: str in globalCache ==> (
    let elems, _ := globalCache[str] in (
        forall k int :: 0 <= k && k < len(elems) ==> (acc(&elems[k]) &&
        (forall str2 string :: str2 in globalCache && str != str2 ==> (let elems2,_ := globalCache[str2] in (forall k2 int :: 0 <= k2 && k2 < len(elems2) ==> (globalFooCache[elems[k]] != globalFooCache[elems2[k2]])))) && 
        acc(globalFooCache[elems[k]])))))
func test_map_slice_injective() {
}