Fix policy for merging subproofs (#6981)

Fix policy for merging subproofs (#6981)

This makes it so that we replace subproof A with subproof B if A and B prove the same thing, and B contains no assumptions. This is independent of the scope that A and B are in.

The previous policy replaced subproof A with subproof B if A and B prove the same thing and were in the same scope. This is not safe if A occurs in multiple scopes, where free assumptions can escape.

The new policy is more effective and safer than the previous one.