Axiom isInfiniteDecidable : forall r, {isInfinite r}+{~isInfinite r}.
