proposition: Lemma lseg_empty xs p q : empty \In lseg p q xs -> p = q /\ xs = [::].
proof: Proof. case:xs=>[|x xs] /=; [by case | case=>r [h][]]. by move/esym; case/un0E; move/empbE; rewrite empPt. Qed.
imports: mathcomp(ssreflect ssrbool eqtype seq ssrfun) LemmaOverloading(heaps rels hprop stmod stsep stlogR)