Fixed a bug in the type system that caused a null pointer exception when reasoning about Entity.  Added a couple more proof rules.  Obvious_Flip_Realiz, Do_Nothing_Realiz, and Iterative_Append_Realize can all be proved interactively now.