notation for multiple substitution

We currently have HasSubstitution, providing the notation t [x := t'] for (named) substitutions. We will inevitably need notions of multiple substitution, such as in the upcoming PRs for STLC strong normalization. The natural extension is t [x := t', y := t'', z := t''']. In other proof assistants, sometimes what is done is having separate classes up to some fixed arity, but in Lean to do this generally is not so hard.

The main questions are making "multiple" general enough to not force an implementation style and being compatible with single substitution still.

(When we have a need for them, we should also make sure unnamed substitutions like t[ t' ] and t [ t', t'', t'''] also align with this)