ea8ecfd390
replace_target uses id_locked.
The id_locked solution is more robust because simp may build a proof
using refl lemmas, but type_context may not be able to establish that
the previous and new target are definitionally equal.
@Armael This commit fixes the issue in the KreMLin proof you showed me.
Now, the following tactic succeeds (as expected)
```
simp [lowstar_semantics.apply_ectx],
```
and the resulting goal is
```
...
|- exp.subbuf (exp.loc (b, n, list.nil field)) a_1 = exp.subbuf ↑?m_1 ?m_2
```
|
||
|---|---|---|
| .. | ||
| data | ||
| init | ||
| smt | ||
| system | ||
| tools/debugger | ||
| .project | ||
| leanpkg.path | ||
| library.md | ||
| standard.lean | ||