notation for multiple substitution

[chenson2018]

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)

[ctchou]

Wouldn't unnamed multiple substitution require some default ordering of free variables?

[chenson2018]

Roughly yes, and I was being a bit cavalier with renaming versus substitution. We won't have this unnamed variant for a bit, so I've not thought it over too carefully yet.