## type invariant preservation question

I have a quite simple question about the behavior of type invariant. In the simple program below, I am asked by the tool to prove a type invariant inside function `g`

for variable `e`

(after split). I would have expected this invariant to be ensured in the proof for `f`

. Is there a way to tell the tool "at this point of program type invariants should hold" ?

```
module Example
type r = { mutable p: int }
invariant { p = 42 }
let f (e: r)
writes {e}
ensures { true }
=
e.p <- 42
let g ()
diverges
=
let e: r = { p = 42 } in
while true do
f (e);
done
end
```

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information