proposition: Fact tagged_hasChoice : hasChoice {i : I & T_ i}.
proof: Proof. pose mkT i (x : T_ i) := Tagged T_ x. pose ft tP n i := omap (mkT i) (find (tP \o mkT i) n). pose fi tP ni nt := obind (ft tP nt) (find (ft tP nt) ni). pose f tP n := if dc n is [:: ni; nt] then fi tP ni nt else None. exists f => [tP n u | tP [[i x] tPxi] | sP sQ eqPQ n]. - rewrite /f /fi; case: (dc n) => [|ni [|nt []]] //=. case: (find _ _) => //= [i]; rewrite /ft. by case Df: (find _ _) => //= [x] [<-]; have:= correct Df. - have /complete[nt tPnt]: exists y, (tP \o mkT i) y by exists x. have{tPnt}: exists j, ft tP nt j by exists i; rewrite /ft; case: find tPnt. case/complete=> ni tPn; exists (code [:: ni; nt]); rewrite /f codeK /fi. by case Df: find tPn => //= [j] _; have:= correct Df. rewrite /f /fi; case: (dc n) => [|ni [|nt []]] //=. rewrite (@extensional _ _ (ft sQ nt)) => [|i]. by case: find => //= i; congr (omap _ _); apply: extensional => x /=. by congr (omap _ _); apply: extensional => x /=. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)