+ (*CSC: ANSWER: it hurts performances since it is possible to *)
+ (*CSC: have an exponential explosion of the size of the proof.*)
+ (*CSC: However, without this bit of reduction some "apply" in *)
+ (*CSC: the library fail (e.g. nat/nth_prime.ma). *)