proposition: Lemma finprod_ext' (xs : seq A) (fs1 fs2 : FinProd' T xs) : uniq xs -> fs1 = fs2 <-> forall a (pf : a \in xs), sel' pf fs1 = sel' pf fs2.
proof: Proof. move=>U; split=>[->|] //. elim: xs U fs1 fs2=>[_ [][]//|x xs IH /= /andP [Ux U][f1 fs1][f2 fs2] H]. case: decP (H x)=>// eqf; rewrite !eqc => ->; last by rewrite inE eq_refl. rewrite (IH U fs1 fs2) // => a pf. have N : a <> x by move=>E; rewrite -E pf in Ux. have xpf : a \in x :: xs by rewrite inE pf orbT. case: decP (H a xpf)=>// qf; move: {qf} (mem_cdr _ _)=>qf. by rewrite (pf_irr pf qf). 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)