proposition: Lemma lseg_null xs q h : valid h -> h \In lseg null q xs -> [/\ q = null, xs = [::] & h = Unit].
proof: Proof. case: xs=>[|x xs] D /= H; first by case: H=><- ->. case: H D=>r [h'][->] _. by rewrite validPtUn. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype seq ssrfun) fcsl(prelude pred pcm unionmap heap) HTT(stmod stsep stlog stlogR)