Checks if a term is safe to inline multiple times
Main inlining function
Implements capture-avoiding substitution [x -> s]t