add equiv and equiv composition structures. useful? at least it gives a way to break up the proof