proposition: Lemma model_runs p y m (e : ST) : m \In model e p y <-> exists i, i \In id_val p /\ (i, y, m) \In runs_of (model e).
proof: Proof. case: e=>mod M S H; rewrite M; split; case=>i [H1] H2. - by exists i; split=>//; exists (bound H1). exists i; exists H1; case: H2 =>/= H2. by rewrite (proof_irrelevance H2 (bound H1)). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) LemmaOverloading(prelude heaps rels hprop domains)