Parameterize the lifetime logic over the user mask.

See merge request !24

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.

This reverts commit a9f50489.

This reverts commit f4a6ea09.

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

Improve notations for functions

See merge request !23

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

Update iris dependency

See merge request !22

using Tej's script from iris!594 (comment 60292)

add GhostCell proof

See merge request !19