Need spurious bind to make function check

[mtzguido]

assume val p : int
assume val q : int
assume val foo : int -> slprop
assume val lem () : Lemma (foo p == foo q)

ghost
fn test ()
  requires foo p
  ensures  foo q
{
  lem();
  // ()
}

This function fails to check:

- Cannot prove:
    foo q
- In the context:
    foo p

But uncommenting the extra (), or doing anything, will make it work. I think without it, the lemma is not eliminated into the context and so is not in scope for the query foo p == foo q.

[gebner]

Yes, I believe that's because we only run the elimination logic at the beginning of a statement, not after it. https://github.com/FStarLang/pulse/blob/0b457c21b9bfe383275ac3f33a87b1eefd75231a/src/checker/Pulse.Checker.fst#L149-L154

It's the same reason why you have to write (); show_proof_state instead of show_proof_state.