A Theory of Explicit Substitutions with Safe and Full Composition