(*CSC: Hmmm. This bit of reduction is not in the spirit of *)
(*CSC: first order unification. Does it help or does it harm? *)
(*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). *)
(*CSC: Hmmm. This bit of reduction is not in the spirit of *)
(*CSC: first order unification. Does it help or does it harm? *)
(*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). *)