first_iso_phi_hits_image

forall (G : Sort succ u), forall (H : Sort succ v), forall (f : forall (x : G), H), forall (q : @KerQuot.{u,v} G H f), @ImagePred.{succ u,succ v} G H f (@KerQuotToH.{u,v} G H f q)

fun G => fun H => fun f => @Quotient.indProp.{u} G (@KerSetoid.{u,v} G H f) (fun (q : @KerQuot.{u,v} G H f) => @ImagePred.{succ u,succ v} G H f (@KerQuotToH.{u,v} G H f q)) (fun (a : G) => @image_intro.{succ u,succ v} G H f a)