proposition: Lemma lseq_null xs h : valid h -> h \In lseq null xs -> xs = [::] /\ h = Unit.
proof: Proof. by move=>D; case/(lseg_null D)=>_ ->. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype seq ssrfun) fcsl(prelude pred pcm unionmap heap) HTT(stmod stsep stlog stlogR)