Add equality type.

Using heterogeneous equality so that we can elaborate
patterns to eliminators later.