proposition: Fact seq_hasChoice : hasChoice (seq T).
proof: Proof. pose r f := [fun xs => fun x : T => f (x :: xs) : option (seq T)]. pose fix f sP ns xs {struct ns} := if ns is n :: ns1 then let fr := r (f sP ns1) xs in obind fr (find fr n) else if sP xs then Some xs else None. exists (fun sP nn => f sP (dc nn) nil) => [sP n ys | sP [ys] | sP sQ eqPQ n]. - elim: {n}(dc n) nil => [|n ns IHs] xs /=; first by case: ifP => // sPxs [<-]. by case: (find _ n) => //= [x]; apply: IHs. - rewrite -(cats0 ys); elim/last_ind: ys nil => [|ys y IHs] xs /=. by move=> sPxs; exists 0; rewrite /= sPxs. rewrite cat_rcons => /IHs[n1 sPn1] {IHs}. have /complete[n]: exists z, f sP (dc n1) (z :: xs) by exists y. case Df: (find _ n)=> // [x] _; exists (code (n :: dc n1)). by rewrite codeK /= Df /= (correct Df). elim: {n}(dc n) nil => [|n ns IHs] xs /=; first by rewrite eqPQ. rewrite (@extensional _ _ (r (f sQ ns) xs)) => [|x]; last by rewrite IHs. by case: find => /=. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)