By default this parameter is filed by the namespace lft_userN. The old method, hard-wiring this parameter to lft_userN, had the defect of requiring to place libraries' namespacec in it *in advance*. The weak branch has always used such a parameter.

We use fnrec: for recursive functions and fn: for non-recursve functions. This is both shorter and closer to Rust.

strengthen lifetime logic: make lft_userN disjoint from lftN so it remains available during atomic accessors

This commit makes typed_val and typed_instruction_ty a definition. Together
with the previous commit on notations for contexts, this seems to fix all
notations issues.

Instead, I have added subscripts to the inclusion notations. This makes pretty
printing much more reliable, and generally even shortens things, as no scope
annotations are needed.

make it so that we can give the option type (instead of the list of variants) to the type_sum lemmas

also update Iris