proposition: Lemma big_setID A B F : \big[aop/idx]_(i in A) F i = aop (\big[aop/idx]_(i in A :&: B) F i) (\big[aop/idx]_(i in A :\: B) F i).
proof: Proof. rewrite (bigID [in B]) setDE. by congr (aop _ _); apply: eq_bigl => i; rewrite !inE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)