Hello once again ! I’ve created this topic to be more specific about one question in particular :

I’m trying to proof this theorem from the book software foundation hoare.v :

```
Theorem assert_assume_differ : exists P b Q,
({{P}} ASSUME b {{Q}})
/\ ~ ({{P}} ASSERT b {{Q}}).
Proof.
exists (fun st => True).
exists (BFalse).
exists (fun st => False).
```

I don’t see how to finish the proof, would you have any idea?