Prove some uniqueness theorems

[Ailrun]

We do not really have type uniqueness because of cumulativity, but we at least need the following:

If G |- M : Π A B and G |- M : Π A' B', then G |- A ≈ A' : Type@j for some j. (1)

Why? Let's think about the following type inference process for application M N:

1. Infer a type A of M under G
2. Get B and C satisfying G |- Π B C ≈ A : Type@i for some i
3. Check N whether it is of B under G
4. Return C[Id,,N]

The problem here is on step 3. What if N is not of B? To get a complete algorithm, we need to show

If G |- M : Π B C is true but G |- N : B is false, G |- M N : D is false for any D (2)

However, without the theorem (1) above, we don't know if there is G |- M : Π B' C' while G |- N : B' is also true (and if this is the case (2) is not true and the algorithm is incomplete)

I think (1) can be proved by the normal form of a function. Our lambda syntax contain a type annotation for its argument, and that should guarantee the equivalence between all possible types. (this isn't the case)

[Ailrun]

Or maybe what we need is a more lenient judgement than type subsumption so that we indeed have (directed) uniqueness modulo that judgement.

[Ailrun]

It is actually easier to define such a judgement (that subsumes type subsumption) for completeness

[Ailrun]

120 is more fundamental.