Acts like have, but removes a hypothesis with the same name as
this one if possible. For example, if the state is:
Then after replace h : β the state will be:
case h
f : α → β
h : α
⊢ β
f : α → β
h : β
⊢ goal
whereas have h : β would result in:
case h
f : α → β
h : α
⊢ β
f : α → β
h✝ : α
h : β
⊢ goal
Equations
- One or more equations did not get rendered due to their size.