rewrite [<|>] sterm pattern

p must be the proof of an equality, possibly under some hypotheses.

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.

It opens one new sequent for each hypothesis of the equality proved by p that is not closed by unification.