Files used in lectures 08 & 09:

nslpk.mod
invariants.mod
template.mod
proof1.mod
proof3.mod
proof4.mod
proof8.mod
proof9.mod

Possible solustions of the exercises of lectures 08 & 09:

nslpk.mod
invariants.mod
template.mod
proof1.mod
proof2.mod
proof3.mod