proposition: Lemma big_mksub_cond {P : pred T} {F : T -> S} (r : seq T): uniq r -> (forall x, x \in r -> P x -> sT x) -> \big[op/idx]_(x <- r | P x) (F x) = \big[op/idx]_(x : I | P (val x) && (val x \in r)) (F (val x)).
proof: Proof. move=> uniq_r h; rewrite -big_filter; apply/esym. pose Q x := P x && (x \in r); rewrite -(big_map val Q). rewrite -big_filter; apply/perm_big/uniq_perm; try rewrite filter_uniq // (map_inj_uniq val_inj). by rewrite /index_enum -enumT enum_uniq. move=> x; rewrite !mem_filter {}/Q; apply/andb_idr. rewrite andbC; case/andP=> /h {}h /h sT_x. apply/mapP; exists (Sub x sT_x). by rewrite /index_enum -enumT mem_enum. by rewrite SubK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset order) mathcomp(ssralg)