This lift function lifts a `relabelling' function between two finite sets along fs, without capturing fz.
Next: lift that function | Prev: John Major equality | Up: contents