proposition: Lemma llist_prec A p (l1 l2 : seq A) h1 h2 g1 g2 : valid (h1 \+ g1) -> llist p l1 h1 -> llist p l2 h2 -> h1 \+ g1 = h2 \+ g2 -> [/\ l1 = l2, h1 = h2 & g1 = g2].
proof: Proof. move=>V H1 H2 E; elim: l1 l2 h1 h2 p H1 H2 E V=>[|a1 l1 IH]. - case=>[|a2 l2] h1 h2 p /= [->->]. - by case=>_ ->; rewrite !unitL. by case=>r [h'][-> _ ->] /validL /validPtUn_cond. case=>[|a2 l2] h1 h2 p /= [p1][k1][-> H1]. - by case=>->-> _ /validL /validPtUn_cond. case=>p2 [k2][-> H2]; rewrite -!joinA => E V. case: {E V} (hcancelV V E) H1 H2; case=>->-> V E H1 H2. by case: (IH _ _ _ _ H1 H2 E V)=>->->->. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat eqtype seq path) pcm(options axioms finmap) pcm(pcm unionmap)