## Restricting behavior of rewrite_list

Hello,

Currently `rewrite_list`

uses the argument `with_terms`

but I think it is difficult for the user to understand what these with_terms corresponds to with this transformation. This list of terms is supposed to be used by `apply/rewrite`

after matching. For example,

```
module Rewrite
use int.Int
function f int : int
predicate p int
axiom A: forall a. f (a+1) = f 42
axiom B: forall a. f a = f (43 + 1)
goal g : 5 = f 42
end
```

`rewrite <- A with 43 (* To instantiate a *)`

`rewrite <- B with 43 (* To instantiate a *)`

To me, it makes less sense to try to do the same when rewriting several hypothesis at once:
`rewrite_list <- A,B with 43`

Also, I am not sure that it works when trying to instantiate with a different value for A and B. Should we remove this feature ?

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information