Hi, I remarked the following (odd?) behaviour of blast and auto : Although they prove the general form:
~ P y ==> P x ==> ~ x = y they can't for the special instance: ~ P (0::nat) ==> P x ==> ~ x = 0 I suspect this is due to an implicit classet rule such as ~ x = (0::nat) = x > 0. Is there a simple way to "correct" this behavious, if it might be considered erronous? Cheers, Amine.
