proposition: Lemma cast_map_cond (T: Type) n m (P : pred 'I_n) (F : 'I_n -> T) (H : m = n) : [seq F i | i <- enum 'I_n & P i] = [seq F (cast_ord H i) | i <- enum 'I_m & P (cast_ord H i) ].
proof: Proof. subst m; have /eq_filter -> : (fun i : 'I_n => P (cast_ord (erefl n) i)) =1 P by move=> i; rewrite /= cast_ord_id. by have /eq_map -> : (fun i : 'I_n => F (cast_ord (erefl n) i)) =1 F by move=> i; rewrite /= cast_ord_id. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype finfun fintype choice seq tuple) mathcomp(finset tuple bigop) tools