Bug fixes, clean ups, finished J operator

TODO check inductive definitions more thoroughly:
 - constructor may not have a parameter of class type
 - recursive TC may only occur on top level