proposition: Lemma locality p q i1 m h : def (i1 :+ h) -> (p # top) i1 -> (p --o q) (i1 :+ h) m -> exists m1, m = m1 :+ h /\ def m /\ (p --o q) i1 m1.
proof: Proof. move=>D [h1][h2][E][H1] _ H2; rewrite {i1}E in D H2 *. move: (H2 h1 (h2 :+ h)); rewrite unA; case/(_ (erefl _) D H1)=>m1 [E][D2]. rewrite {m}E unA in H2 D2 *; exists (m1 :+ h2); do !split=>//. by apply: antiframe D H2. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun seq eqtype) LemmaOverloading(heaps rels hprop stmod)