Shrink IBCs dramatically

By erasing types, and inlined definitions which are only used for
totality checking so really don't need storing.