proposition: Lemma zunit_supp f : supp (zip_unit f) = supp f.
proof: Proof. case: f=>s H; rewrite /supp /= {H}. by elim: s=>[|[k v] s IH] //=; rewrite IH. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)