proposition: Lemma fr_pre p i j : (p # top) i -> (p # top) (i :+ j).
proof: Proof. by case=>i1 [i2][->][H] _; rewrite -unA; exists i1; exists (i2 :+ j). Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun seq eqtype) LemmaOverloading(heaps rels hprop stmod)