proposition: Lemma mapf_disjL s1 s2 s : mapf s1 = mapf s2 -> disj s1 s = disj s2 s.
proof: Proof. case: s1 s2 s=>s1 S1 [s2 S2][s S] /fmapE /=. elim: s1 S1 s2 S2 s S=>[|[k v] s1 IH] /= S1; case=>//= [[k2 v2]] s2 S2 s S. case=>E _; rewrite -{k2}E in S2 *. move/(IH (path_sorted S1) _ (path_sorted S2) _ S). by rewrite /disj /supp /= => ->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)