Fix some non-terminating proofs that agsy snuck in