Gobra cannot prove that a func literal is non-nil

[jcp19]

Below, we have a snippet from VerifiedSCION. One would expect that the last assert succeeds, but Gobra is not able to prove it.

	verScionTemp :=
		// @ requires acc(&key, _) && acc(sl.AbsSlice_Bytes(key, 0, len(key)), _)
		// @ requires scrypto.ValidKeyForHash(key)
		// @ ensures  acc(&key, _) && acc(sl.AbsSlice_Bytes(key, 0, len(key)), _)
		// @ ensures  h != nil && h.Mem()
		// @ decreases
		func /*@ f @*/ () (h hash.Hash) {
			mac, _ := scrypto.InitMac(key)
			return mac
		}
	// Gobra cannot currently prove the following assertion, even though it must
	// follow from the structure of the declaration of `verScionTemp`.
	// @ assert verScionTemp != nil