Proved correctness of prop_exec_preserves_well_formed checker

... under some strong (but natural) assumptions about genState

In the meanwhile run into some very silly unification problem,
that Zoe previously hacked around by adding overlapping type
class instances. The main problem is that Coq can't figure out
"Testable (Property Gen)" although it knows "Testable (Gen QPred)"
and Property is defined as follows:
Definition Property (Gen: Type -> Type) : Type := Gen QProp.
Ended up adding lots of silly type annotations to work around
Coq's silliness.