proposition: Lemma big_mksub {F : T -> S} (r : seq T): uniq r -> (forall x, x \in r -> sT x) -> \big[op/idx]_(x <- r) F x = \big[op/idx]_(x : I | val x \in r) F (val x).
proof: Proof. by move=> uniq_r h; apply/big_mksub_cond=> // x /h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset order) mathcomp(ssralg)