Prove cumulativity

[Ailrun]

Why is this so short...
I originally planed to add a separate module Cumulativity.v and expected something more involved, but guess what, this (less than) 20 line happened, and it does not make much sense to put just this single proofs (even with some corollaries) to live in a separate module.

[HuStmpHrrr]

I am also a bit surprised, but it makes sense
the theorem states that we have a fixed R to relate values, whereas in Agda, R is a result of recursion computed by El. In Agda, we cannot fix the relation between values but in Coq we can. I think it's a pleasant distinction caused by impredicativity.

[HuStmpHrrr]

Closes #64

[Ailrun]

Oops, I forgot to put that on the description 😅