## Forall construction in code for ghost binding

Sometimes when we want to prove such functions:

```
let f x : result
ensures { forall y. P(x,y) -> Q(x,y) }
```

We need to prove with a ghost variable, for easing the proof

```
let f' x (ghost y) : result
requires { P(x,y) }
ensures { Q(x,y) }
```

However it is not possible to prove the first function using the second. We propose to add a new construction which allows it.

```
let f x : result
ensures { forall y. P(x,y) -> Q(x,y) }
=
forall y requires { P(x,y) } in
f' x y
```

The semantic of this function is not completely clear:

- should a VC be generated to check that it exists such
`y`

- what if the result contains a ghost
- what if there are ghost effect

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