Remove dependency of fancy updates on the program language.

This merge request removes the dependency on the program language from the encoding of invariants, fancy updates, and many constructions such as boxes, sts, auth, ... This reason for doing this, is that in some cases one might not want to use the Iris definition of weakest preconditions or the Iris interface for a programming language.

I have achieved this factoring out a type class invG that keeps track of the ghost state needed for encoding invariants from the type class irisG. Fancy updates, boxes and sts are parametrized by invG, and not by irisG (which depends on the language).

TODO: state adequacy for fancy updates in a self-contained way.