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