Begin translation from annotated syntax to concise syntax
Begin translation from annotated syntax to concise syntax

This is before we can even consider doing the opposite. This will help us making sense of the elaboration.
The proof is still incomplete.
Also we also use the nasty trick of posing TyEl in our particular case so we can compute it.

TheoWinterhalter/formal-type-theory