Added two rules to the prover to get Test02 in test01.star to go through.
One rule substitutes logical variables with program variables to which they are known to be equal.
One rule tests if the spatial parts of both sides of the sequent are equal and if so proceeds to look at the pure parts.

These rules might be somewhat specialized to the problem. In particular the first one might not do be clever if some program variables are euqal to each other; it just does substitution, no fancy unification. And the second rule uses conservative heuristics to be sound but might not pull out all pure parts.