Axiom isNaNDecidable : forall r, {isNaN r}+{~isNaN r}.
