proposition: Lemma first_exists A p h (ls : seq A) : p != null -> llist p ls h -> exists x r h', [/\ ls = x :: behead ls, h = p :-> (x, r) \+ h' & llist r (behead ls) h'].
proof: Proof. case: ls=>[|a ls] /= H []; first by case: eqP H. by move=>r [h'][-> H1]; eexists a, r, h'. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat eqtype seq path) pcm(options axioms finmap) pcm(pcm unionmap)