Inject assumption about independence on ghost parameters

[vkuncak]

We could inject certain free assumptions in verification that correspond to the existence of a stripped down function that is generated during ghost erasure. Given:

def f(x: Int, @ghost y: Int): Int = { ... } ensuring(res => P)

we should be able to postulate in the verification pipeline:

@extern def f_compiled(x: Int): Int
def f(x: Int, @ghost y: Int): Int = { ... } ensuring(res => P && res == f_compiled(x))