proposition: Lemma lseg_add_last xs x p r h : h \In lseg p r (rcons xs x) <-> exists q, exists h', h = h' :+ (q :-> x :+ q .+ 1 :-> r) /\ h' \In lseg p q xs.
proof: Proof. move: xs x p r h. elim=>[|x xs IH] y p r h /=; first by split; case=>x [_][->][<-] ->; hhauto. split. - case=>z [h1][->]; case/IH=>w [h2][->] H1. by exists w; exists (p :-> x :+ (p .+ 1 :-> z :+ h2)); hhauto. case=>q [h1][->][z][h2][->] H1. exists z; exists (h2 :+ q :-> y :+ q .+ 1 :-> r). by rewrite -!unA; split=>//; apply/IH; eauto. Qed.
imports: mathcomp(ssreflect ssrbool eqtype seq ssrfun) LemmaOverloading(heaps rels hprop stmod stsep stlogR)