proposition: Lemma eval_Pick e (qev := qf_eval e) : let P i := qev (pred_f i) in qev Pick = (if pick P is Some i then qev (then_f i) else qev else_f).
proof: Proof. move=> P; rewrite ((big_morph qev) false orb) //= big_orE /=. apply/existsP/idP=> [[p] | true_at_P]. rewrite ((big_morph qev) true andb) //= big_andE /=. case/andP=> /forallP-eq_p_P. rewrite (@eq_pick _ _ P) => [|i]; first by case: pick. by move/(_ i): eq_p_P => /=; case: (p i) => //= /negPf. exists [ffun i => P i] => /=; apply/andP; split. rewrite ((big_morph qev) true andb) //= big_andE /=. by apply/forallP=> i; rewrite /= ffunE; case Pi: (P i) => //=; apply: negbT. rewrite (@eq_pick _ _ P) => [|i]; first by case: pick true_at_P. by rewrite ffunE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)