proposition: Lemma modelE e1 e2 : e1 = e2 <-> model e1 = model e2.
proof: Proof. move: e1 e2=>[e1 H1][e2 H2] /=; split=>[[//]|E]. by subst e2; congr STprog; apply: pf_irr. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)