proposition: Lemma lseg_null xs q h : def h -> h \In lseg null q xs -> [/\ q = null, xs = [::] & h = empty].
proof: Proof. case:xs=>[|x xs] D /= H; first by case: H=><- ->. by case: H D=>r [h'][->] _; rewrite defPtUn eq_refl. Qed.
imports: mathcomp(ssreflect ssrbool eqtype seq ssrfun) LemmaOverloading(heaps rels hprop stmod stsep stlogR)