Efficient Reduction in Coq