@conn_map_elim _ _ _ _ Esurj (fun b => exists c : C, forall a, g a = b -> f a = c) ishprop_surjective_factor_aux (fun a => exist (fun c => forall a, _ -> _ = c) (f a) (fun a' => Eg a' a)).
Require Import