proposition: Lemma fin_undefE (T : finType) (Us : T -> tpcm) (tag : T) : fin_undef = undef :> fin_prod_TPCM Us tag.
proof: Proof. by []. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq bigop fintype finset) pcm(options axioms prelude seqperm pred seqext)