proposition: Lemma modelE (e1 e2 : ST) : e1 = e2 <-> model e1 = model e2.
proof: Proof. move: e1 e2=>[e1 M1 S1 H1][e2 M2 S2 H2] /=; split=>[[//]|E]. rewrite E in M1 S1 H1 *. by congr STprog; apply: proof_irrelevance. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) LemmaOverloading(prelude heaps rels hprop domains)