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.

pulse/src/checker/Pulse.Checker.fst

Lines 149 to 154 in 0b457c2

	= if Pulse.Checker.AssertWithBinders.handle_head_immediately t
	then Pulse.Checker.AssertWithBinders.check g0 pre0 pre0_typing post_hint res_ppname t check
	else (
	let (| g, pre, pre_typing, k_elim_pure |) =
	Pulse.Checker.Prover.elim_exists_and_pure pre0_typing
	in

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