More Derived
Replace subst with elimEq, and remove old proj1/2 replaced by elimPair.

Actually, because this is heterogeneous equality and the motive
does not take a type B as an argument, this is a subtle variant
of K #muahahahahahahha