[michocoq] Redefine set.remove so that it computes

Before this MR, set.remove uses List.remove which only computes when its decide_equality argument does. We passed it an opaque lemma so it did not compute. Moreover, it always scanned the whole list but since we only apply it on sorted lists it could stop as soon as it encounters a value larger than the one to remove.

This MR redefines set.remove so that it does not depend on decidability of equality anymore and returns as soon as it can.