first_iso_phi_injective

forall (G : Sort succ u), forall (H : Sort succ v), forall (f : forall (x : G), H), forall (q1 : @KerQuot.{u,v} G H f), forall (q2 : @KerQuot.{u,v} G H f), forall (h : @Eq.{succ v} H (@KerQuotToH.{u,v} G H f q1) (@KerQuotToH.{u,v} G H f q2)), @Eq.{succ u} (@KerQuot.{u,v} G H f) q1 q2

fun G => fun H => fun f => @Quotient.indProp.{u} G (@KerSetoid.{u,v} G H f) (fun (q1 : @KerQuot.{u,v} G H f) => forall (q2 : @KerQuot.{u,v} G H f), forall (h : @Eq.{succ v} H (@KerQuotToH.{u,v} G H f q1) (@KerQuotToH.{u,v} G H f q2)), @Eq.{succ u} (@KerQuot.{u,v} G H f) q1 q2) (fun (a : G) => @Quotient.indProp.{u} G (@KerSetoid.{u,v} G H f) (fun (q2 : @KerQuot.{u,v} G H f) => forall (h : @Eq.{succ v} H (@KerQuotToH.{u,v} G H f (@KerQuotMk.{u,v} G H f a)) (@KerQuotToH.{u,v} G H f q2)), @Eq.{succ u} (@KerQuot.{u,v} G H f) (@KerQuotMk.{u,v} G H f a) q2) (fun (b : G) => fun (h : @Eq.{succ v} H (@KerQuotToH.{u,v} G H f (@KerQuotMk.{u,v} G H f a)) (@KerQuotToH.{u,v} G H f (@KerQuotMk.{u,v} G H f b))) => @ker_quot_sound.{u,v} G H f a b h))