Extensional TT as formulated is not suitable for automated unification

[Russoul]

I've hit this problem while working on #6.
When solving a unification problem of the sort:

Σ₀ (Γ ⊦ ? : A) Σ₁ (Γ ⊦ ? = t : A)

We need to be able to check whether t can be typed in Σ₀, otherwise we wouldn't be able to instantiate ?.
But checking that can't be automated because t might depend on equality assumptions in Σ₁. That dependence in not reflected in t itself (so forgotten) and can't be reconstructed either (theoretically impossible due to presence of equality reflection). Hence that part of unification is not amenable to automation. Hence unification overall is not amenable to automation.

We have to resolve this somehow if we hope to have a usable language. What's certain is that the foundation doesn't cut it as is and must be rethought.