Acts like have, but removes a hypothesis with the same name as
this one if possible. For example, if the state is:
f : α → β
h : α
⊢ goal
Then after replace h := f h the state will be:
f : α → β
h : β
⊢ goal
whereas have h := f h would result in:
f : α → β
h† : α
h : β
⊢ goal
This can be used to simulate the specialize and apply at tactics of Coq.
Equations
- One or more equations did not get rendered due to their size.