Comments out the FOR part of Imp.v
Part way through Equiv