proposition: Lemma found_pf k : partition_axiom k Unit (found_tag k).
proof: Proof. by rewrite /partition_axiom unitR. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat eqtype seq path) pcm(options axioms finmap) pcm(pcm unionmap)