I believe (and please correct me if I am wrong) that most presentations of Martin-Löf Type Theory satisfy the following property, or something very close to it.
Given a derivation tree with conclusion $\Gamma \vdash a : A$ and a derivation tree with conclusion $\Delta, x : A \vdash t : T$, we can find a derivation tree with conclusion $\Delta, \Gamma \vdash t[x \leftarrow a] : T[x \leftarrow a]$.
Moreover, I suppose one can prove this by a humble induction argument. Alas, that looks like a loooong proof that I would rather not do myself, which leads to my questions.
- Does this property have an official name?
- Does it hold as I stated (or perhaps modulo some additional conditions)?
- What's a good reference which states and proves this property?
Yes, this property is often called "substitution lemma" (also in type systems different from Martin-Löf type theory).
Yes, except that the conclusion should be of the form $\Gamma, \Delta [x \leftarrow a] \vdash t[x \leftarrow a] : T[x \leftarrow a]$ (the substitution percolates also to the context). Actually the exact statement depends on the precise definition of Martin-Löf type theory.
A good reference is Gardner's PhD thesis, in particular the substitution lemma on page 16 (Lemma 2.1.10). Actually, this lemma is not stated for Matin-Löf type theory, but for a simpler pure type system in the same vein (there is no significant difference, at least for the statement and the proof of such a lemma).