Add Properties of Observation Congruence
At least for observation congruence (and possibly for the other relations along the way), the book should check (and possibly prove) that all relevant properties hold, e.g. that it is an equivalence relation, a congruence, termination sensitive, … The lecture has a nice table Holger fills out along the way, maybe the book should have something similar.