Indentation
Alternative way to perform levitation.

Dagand typically levitates Desc and elimDesc,
keeping El, Hyps, and prove primitive.

Instead, we can levitate El, Hyps, and prove,
keeping Desc and elimDesc primitive.

This alternative version has the advantage that it can be
performed in an intrinsically typed theory, whereas Dagand
levitation is limited to extrinsic typing.

The disadvantage is that Desc values must be eliminated with
elimDesc instead of ind.

Note that Agda cannot tell that Fix is strictly positive.
El expands to elimDesc, and Agda cannot see that the "Rec"
branch of elimDesc is strictly positive. In fact, the helper
function El' is defined such that its arguments do not contain
occurrences of Fix, but its return type does. This is a positive
occurrence in the constructor,
similiar to "foo : (Bar → Baz → Foo) → Foo".