Pushing quotients in the completeness proof (first functor done).
	modified:   Completeness.agda