proposition: Lemma lseg_case xs p q h : h \In lseg p q xs -> [/\ p = q, xs = [::] & h = empty] \/ exists x, exists r, exists h', [/\ xs = x :: behead xs, h = p :-> x :+ (p .+ 1 :-> r :+ h') & h' \In lseg r q (behead xs)].
proof: Proof. case:xs=>[|x xs] /=; first by case=>->->; left. by case=>r [h'][->] H; right; hhauto. Qed.
imports: mathcomp(ssreflect ssrbool eqtype seq ssrfun) LemmaOverloading(heaps rels hprop stmod stsep stlogR)