proposition: Lemma fin_choice_aux (T : choiceType) T' (d : T') (R : T -> T' -> Prop) (xs : seq T) : (forall x, x \in xs -> exists y, R x y) -> exists f , forall x, x \in xs -> R x (f x).
proof: Proof. elim: xs. move => _. exists (fun _ => d) => ?. by rewrite in_nil. move => x s IH step. have/IH: forall x : T, x \in s -> exists y, R x y. move => z ins. apply: step. by rewrite in_cons ins orbT. case => f Hf. (case: (step x); first by rewrite mem_head) => y Rxy. exists (fun z => if z == x then y else f z) => z. rewrite in_cons; case/orP. move/eqP=>e. by rewrite -e ?eq_refl in Rxy *. case e: (z == x); first by rewrite (eqP e). exact: Hf. Qed.
imports: mathcomp(all_ssreflect) Relations CompDecModal.libs(edone bcase)