proposition: Lemma lseq_pos xs p h : p != null -> h \In lseq p xs -> exists x, exists r, exists h', [/\ xs = x :: behead xs, p :-> x \+ (p .+ 1 :-> r \+ h') = h & h' \In lseq r (behead xs)].
proof: Proof. case: xs=>[|x xs] /= H []. - move=>E. by rewrite E eq_refl in H. by move=>y [h'][->] H1; heval. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype seq ssrfun) fcsl(prelude pred pcm unionmap heap) HTT(stmod stsep stlog stlogR)