Get rid of the proofs showing that ChainStep and ChainTrace respect
EnvironmentEquiv. ChainTrace no longer respects this in the base case
(this was necessary to define trace_app).