Add missing termination proofs

[jcp19]

Not ready for review yet. There is a strange issue with Gobra that causes the following errors to be reported in package /github/workspace/VerifiedSCION/gobra/lib/slayers when they should not:

15:40:19.425 [main] ERROR viper.gobra.GobraRunner$ - Gobra has found 2 error(s):
15:40:19.431 [main] ERROR viper.gobra.GobraRunner$ - 	<.:0:0> Unfold might fail. 
Permission to s.Mem() might not suffice.
15:40:19.431 [main] ERROR viper.gobra.GobraRunner$ - 	<.:0:0> Unfold might fail. 
Permission to s.Mem() might not suffice.