The following type should not verify; it should give an error tht the :lemma is not a lemma:

typedef struct S {

int x;
_(invariant :lemma \on_unwrap(\this, \false))

} S;

Also, the :lemma appears to not be usable after unwrapping (i.e., you should be able to _(assert \false) after unwrapping an S).