proposition: Lemma def_runs i y m (e : ST) : (i, y, m) \In runs_of (model e) -> [/\ def i, i \In s.1 & def m].
proof: Proof. case=>[[/= P D]] R; split=>//. by case: e R=>p M S H; case: m=>//; move/S. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) LemmaOverloading(prelude heaps rels hprop domains)