proposition: Lemma foldForallP I e : (forall e', {in [predC I], same_env e e'} -> holds e' f) <-> holds e (foldr Forall f I).
proof: Proof. elim: I e => /= [|i I IHi] e. by split=> [|f_e e' eq_e]; [apply | apply: eq_holds f_e => i; rewrite eq_e]. split=> [f_e' x | f_e e' eq_e]; first set e_x := set_nth 0 e i x. apply/IHi=> e' eq_e; apply: f_e' => j. by have:= eq_e j; rewrite nth_set_nth /= !inE; case: eqP. move/IHi: (f_e e'`_i); apply=> j. by have:= eq_e j; rewrite nth_set_nth /= !inE; case: eqP => // ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)