let
iter s f x =
assert
(
Term
.is_var x);
let
(y, _) = find s x
in
f y;
Pre
.iter f (inv s y)