proposition: Lemma fin_ext (fs1 fs2 : FinProd) : (forall a, sel a fs1 = sel a fs2) -> fs1 = fs2.
proof: Proof. move=>H; rewrite (finprod_ext' _ _ (enum_uniq _))=>a pf. by move: (H a); rewrite /sel (pf_irr (mem_enum _ _) pf). Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat seq eqtype choice fintype) pcm(options axioms) Coq(Classes.Morphisms Program.Basics Program.Tactics) Coq(Relations)