proposition: Lemma big_subseqs0 (F : seq T -> R) : \big[*%M/1]_(i : subseqs [::]) F i = F [::].
proof: Proof. transitivity (\big[*%M/1]_(s <- [:: sub_full [::]]) F s); last by rewrite big_seq1. apply: perm_big; apply uniq_perm => //; first exact: index_enum_uniq. by move=> [{}s Hs]; rewrite !inE mem_index_enum -val_eqE /= -subseq0 Hs. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass sorted