Thanks for the link to SPJ's notes, I'll read that tomorrow.

Equivalence of terms is an efficient tool for verification; I suspect that isn't really in the set of goals for Fuse, though.