proposition: Lemma big_subseqs_cons (F : seq T -> R) (a : T) (s : seq T) : uniq (a :: s) -> \big[*%M/1]_(i : subseqs (a :: s)) F i = \big[*%M/1]_(i : subseqs s) F (a :: i) * \big[*%M/1]_(i : subseqs s) F (i).
proof: Proof. move=> asuniq; have := asuniq => /= /andP[_ suniq]. rewrite !big_subseqs //. rewrite [X in X * _](big_subseqs (fun s => F (a :: s))) //. rewrite (bigID (fun m => tnth m ord0)) /=; congr( _ * _). - rewrite [RHS](eq_big (fun m => tnth (cons_tuple true m) ord0) (fun m => F (mask (cons_tuple true m) (a :: s)))) //. apply: (reindex (@cons_tuple _ _ true)); exists (@behead_tuple _ _). + by move=> m _; apply val_inj; case: m => [[|m0 m]]. + by move=> m; rewrite inE; case: m => [[|[|] m]]//= Hm _; exact: val_inj. - rewrite [RHS](eq_big (fun m => ~~ tnth (cons_tuple false m) ord0) (fun m => F (mask (cons_tuple false m) (a :: s)))) //. apply: (reindex (@cons_tuple _ _ false)); exists (@behead_tuple _ _). + by move=> m _; apply val_inj; case: m => [[|m0 m]]. + by move=> m; rewrite inE; case: m => [[|[|] m]]//= Hm _; exact: val_inj. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted