proposition: Lemma all_sig_cond_dep I T (C : pred I) P : (forall x, T x) -> (forall x, C x -> {y : T x | P x y}) -> {f : forall x, T x | forall x, C x -> P x (f x)}.
proof: Proof. by move=> f0 /(all_tag_cond_dep f0)[f]; exists f. Qed.
imports: ssreflect ssrfun