Added prove rule to drop spatial part of hypothesis when conclusion is pure.
This should help the inconsistency check by allowing the smt solver to find the inconsistency if it holds for pure reasons.