Type classes for updates properties
IT turns out that iGPS and alike also need basic and fancy updates, and their properties are very similar (that is, apart from the properties relating them to ownership, they have exactly the same theory). Hence, a lot of proofs and instances can be shared across the several logics.