proposition: Lemma big_map : forall (J : eqType) (h : J -> I) r (P : pred I) F, \big[op/idx]_(i <- map h r | P i) F i === \big[op/idx]_(j <- r | P (h j)) F (h j).
proof: Proof. move=> J h r P F; elim: r;try reflexivity; move=> j r //=. by case: (P (h j)); move=> Heq; rewrite -> Heq; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops