proposition: Lemma big_seq_sub (T : countType) (s : seq T) F : \big[op/idx]_(x : seq_sub s) F (ssval x) = \big[op/idx]_(x <- undup s) F x.
proof: Proof. rewrite -[LHS](big_map (ssval (s := s)) xpredT (fun x : T => F x)). apply perm_big; apply uniq_perm. - rewrite map_inj_uniq; last exact: val_inj. exact: index_enum_uniq. - exact: undup_uniq. - move=> x; rewrite mem_undup; apply/mapP/idP => [/= [y _ ->] | Hx]. + by case: y => y /= Hy. + by exists (SeqSub Hx); rewrite // mem_index_enum. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(finset bigop path binomial)