make the provisional cache slightly less broken
It is still broken for the following cycles:
```mermaid
graph LR
R["R: coinductive"] --> A["A: inductive"]
R --> B["B: coinductive"]
A --> B
B --> R
```
the `R -> A -> B -> R` cycle should be considered to not hold, as it is mixed, but because we first put `B` into the cache from the `R -> B -> R` cycle which is coinductive, it does hold.
This issue will also affect our new coinduction approach. Longterm cycles are coinductive as long as one step goes through an impl where-clause, see f4fc5bae36/crates/formality-prove/src/prove/prove_wc.rs (L51-L62). Here we would first have a fully inductive cycle `R -> B -> R` which is then entered by a cycle with a coinductive step `R -> A -coinductive-> B -> R`.
I don't know how to soundly implement a provisional cache for goals not on the stack without tracking all cycles the goal was involved in and whether they were inductive or not. We could then only use goals from the cache if the *inductivity?* of every cycle remained the same. This is a mess to implement. I therefore want to rip out the provisional cache entirely, but will wait with this until I talked about it with `@nikomatsakis.`
r? `@compiler-errors`
a04dfc32e6