Matita Home

`rewrite dir p patt`

- Synopsis:
- Pre-conditions:
**p**must be the proof of an equality, possibly under some hypotheses.- Action:
It looks in every term matched by

**patt**for all the occurrences of the left hand side of the equality that**p**proves (resp. the right hand side if**dir**is**<**). Every occurence found is replaced with the opposite side of the equality.- New sequents to prove:
It opens one new sequent for each hypothesis of the equality proved by

**p**that is not closed by unification.