Typed self representation is impossible in strongly normalizing languages, WIP

Warning: the definition of typed self-representation is not directly
formalizable, hence our thesis can't be fully proven in Agda. Here we have just
a support lemma.
Replace the insane Data.Maybe (which overloads `just`) to help type inference

We just introduce a custom definition of Maybe.
TypedSelfRepresentation.agda: Clarify the point a bit
Clarify discussion of TSR
ImpredicativePolymorphism.agda: minor improvements