That's because whether or not a side-effect proof of one assumption happens first can determine whether a side-effect of another assumption follows through. For example,
assumptions: (n in N+, x in {1 .. n})
will automatically prove that x in Z. However,
assumptions: (x in {1 .. n}, n in N+)
will not, because at the time of deriving side-effects for the former assumption it doesn't know that n is an integer so it is unable to derive that x is an integer as a side-effect.
With the "readily_provable" feature (#289) which is in progress, this can cause an error to occur because it will recognize that "n in Z" is readily provable but won't be able to prove this until the "n in N+" side-effects occur. This is good in that it will clue the user into the problem; however, the error message is not particularly helpful. We should eventually try to improve user experience for this sort of thing (a more helpful error message or some way to avoid the problem).
That's because whether or not a side-effect proof of one assumption happens first can determine whether a side-effect of another assumption follows through. For example, assumptions: (n in N+, x in {1 .. n}) will automatically prove that x in Z. However, assumptions: (x in {1 .. n}, n in N+) will not, because at the time of deriving side-effects for the former assumption it doesn't know that n is an integer so it is unable to derive that x is an integer as a side-effect.
With the "readily_provable" feature (#289) which is in progress, this can cause an error to occur because it will recognize that "n in Z" is readily provable but won't be able to prove this until the "n in N+" side-effects occur. This is good in that it will clue the user into the problem; however, the error message is not particularly helpful. We should eventually try to improve user experience for this sort of thing (a more helpful error message or some way to avoid the problem).