proposition: Lemma big_index_uniq (I : eqType) (r : seq I) (E : 'I_(size r) -> R) : uniq r -> \big[op/idx]_i E i = \big[op/idx]_(x <- r) oapp E idx (insub (index x r)).
proof: Proof. move=> Ur; apply/esym; rewrite big_tnth. by under [LHS]eq_bigr do rewrite index_uniq// valK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)