Correct arguments to equiv_compose, and simplify equiv_Transitive.

The function arguments to equiv_compose should be explicit.  This makes it unnecessary to break down the arguments to equiv_Transitive, so we can eliminate the auxiliary lemma.