proposition: Lemma big_sub_widen {P : pred T} {F : T -> S}: (forall x, sT x -> rT x) -> \big[op/idx]_(x : I | P (val x)) (F (val x)) = \big[op/idx]_(x : J | P (val x) && sT (val x)) (F (val x)).
proof: Proof. move=> h; pose Q := [pred x | P x && sT x]. rewrite -big_map -(big_map val Q F). rewrite -big_filter -[X in _=X]big_filter; apply/perm_big. apply/uniq_perm; rewrite ?(filter_uniq, map_inj_uniq val_inj) //; try by rewrite /index_enum -enumT enum_uniq. move=> x; rewrite !mem_filter {}/Q inE -andbA; congr (_ && _). apply/idP/andP; last first. by case=> sTx _; apply/mapP; exists (Sub x sTx); rewrite ?SubK. case/mapP=> y _ ->; split; first by apply valP. apply/mapP; exists (Sub (val y) (h _ (valP y))). 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)