prove one of the EqualityType theorems

about six more to go :/