proposition: Lemma foldExistsP I e : (exists2 e', {in [predC I], same_env e e'} & holds e' f) <-> holds e (foldr Exists f I).
proof: Proof. elim: I e => /= [|i I IHi] e. by split=> [[e' eq_e] |]; [apply: eq_holds => i; rewrite eq_e | exists e]. split=> [[e' eq_e f_e'] | [x]]; last set e_x := set_nth 0 e i x. exists e'`_i; apply/IHi; exists e' => // j. by have:= eq_e j; rewrite nth_set_nth /= !inE; case: eqP => // ->. case/IHi=> e' eq_e f_e'; exists e' => // 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)