first_iso_phi_surj_image

forall (G : Sort succ u), forall (H : Sort succ v), forall (f : forall (x : G), H), forall (y : H), forall (hy : @ImagePred.{succ u,succ v} G H f y), forall (P : Prop), forall (mk : forall (q : @KerQuot.{u,v} G H f), forall (h : @Eq.{succ v} H (@KerQuotToH.{u,v} G H f q) y), P), P

fun G => fun H => fun f => fun y => fun hy => fun P => fun mk => @image_elim.{succ u,succ v} G H f y hy P (fun (a : G) => fun (h : @Eq.{succ v} H (f a) y) => mk (@KerQuotMk.{u,v} G H f a) (@eq_trans.{succ v} H (@KerQuotToH.{u,v} G H f (@KerQuotMk.{u,v} G H f a)) (f a) y (@ker_quot_to_h_mk.{u,v} G H f a) h))