Some way of blocking `simp` from unifying schematics

[Xaphiosis]

As seen in https://github.com/seL4/l4v/issues/729 if wp or some other tool gets you into a bad situation, e.g. schematic assumption, simp will happily unify that with False which will result in very bad outcomes in wp proofs. clarsimp of course prevents this problem, but it involves clarify and so blows up ∃val. x = Some val to introduce a free variable that a precondition schematic doesn't rely on, creating the problem for wp and simp to make worse. So in these cases we need simp, but without having it instantiate schematics.

If we have a safer wp, a safer vcg and a safer simp, we have some weaponry in stabilising some of the more horrid ccorres proofs like the fastpath ones.

[lsf37]

This one I have slightly less hope for -- it's likely that we'd have to go deep into the guts of simp to prevent it from instantiating schematics and changing fundamental simp behaviour is going to be very subtle.

That said, one avenue of exploration could be to look at how clarsimp prevents simp from instantiating schematics and see if that could be extracted somehow into a new method.