RingChineseRemainder

forall (R : Sort succ u), forall (zeroR : R), forall (oneR : R), forall (addR : forall (a : R), forall (b : R), R), forall (negR : forall (a : R), R), forall (subR : forall (a : R), forall (b : R), R), forall (mulR : forall (a : R), forall (b : R), R), forall (RI : Sort succ v), forall (zeroI : RI), forall (oneI : RI), forall (addI : forall (a : RI), forall (b : RI), RI), forall (negI : forall (a : RI), RI), forall (subI : forall (a : RI), forall (b : RI), RI), forall (mulI : forall (a : RI), forall (b : RI), RI), forall (RJ : Sort succ w), forall (zeroJ : RJ), forall (oneJ : RJ), forall (addJ : forall (a : RJ), forall (b : RJ), RJ), forall (negJ : forall (a : RJ), RJ), forall (subJ : forall (a : RJ), forall (b : RJ), RJ), forall (mulJ : forall (a : RJ), forall (b : RJ), RJ), forall (P : Sort succ p), forall (zeroP : P), forall (oneP : P), forall (addP : forall (a : P), forall (b : P), P), forall (negP : forall (a : P), P), forall (subP : forall (a : P), forall (b : P), P), forall (mulP : forall (a : P), forall (b : P), P), forall (pair : forall (x : RI), forall (y : RJ), P), forall (fst : forall (z : P), RI), forall (snd : forall (z : P), RJ), forall (modI : forall (x : R), RI), forall (modJ : forall (x : R), RJ), forall (ringR_args : @RingLawArgs.{succ u} R zeroR oneR addR negR subR mulR), forall (ringP_args : @RingLawArgs.{succ p} P zeroP oneP addP negP subP mulP), Prop

def RingChineseRemainder.{p,u,v,w} :
  forall (R : Sort succ u), forall (zeroR : R), forall (oneR : R), forall (addR : forall (a : R), forall (b : R), R), forall (negR : forall (a : R), R), forall (subR : forall (a : R), forall (b : R), R), forall (mulR : forall (a : R), forall (b : R), R), forall (RI : Sort succ v), forall (zeroI : RI), forall (oneI : RI), forall (addI : forall (a : RI), forall (b : RI), RI), forall (negI : forall (a : RI), RI), forall (subI : forall (a : RI), forall (b : RI), RI), forall (mulI : forall (a : RI), forall (b : RI), RI), forall (RJ : Sort succ w), forall (zeroJ : RJ), forall (oneJ : RJ), forall (addJ : forall (a : RJ), forall (b : RJ), RJ), forall (negJ : forall (a : RJ), RJ), forall (subJ : forall (a : RJ), forall (b : RJ), RJ), forall (mulJ : forall (a : RJ), forall (b : RJ), RJ), forall (P : Sort succ p), forall (zeroP : P), forall (oneP : P), forall (addP : forall (a : P), forall (b : P), P), forall (negP : forall (a : P), P), forall (subP : forall (a : P), forall (b : P), P), forall (mulP : forall (a : P), forall (b : P), P), forall (pair : forall (x : RI), forall (y : RJ), P), forall (fst : forall (z : P), RI), forall (snd : forall (z : P), RJ), forall (modI : forall (x : R), RI), forall (modJ : forall (x : R), RJ), forall (ringR_args : @RingLawArgs.{succ u} R zeroR oneR addR negR subR mulR), forall (ringP_args : @RingLawArgs.{succ p} P zeroP oneP addP negP subP mulP), Prop :=
  fun R => fun zeroR => fun oneR => fun addR => fun negR => fun subR => fun mulR => fun RI => fun zeroI => fun oneI => fun addI => fun negI => fun subI => fun mulI => fun RJ => fun zeroJ => fun oneJ => fun addJ => fun negJ => fun subJ => fun mulJ => fun P => fun zeroP => fun oneP => fun addP => fun negP => fun subP => fun mulP => fun pair => fun fst => fun snd => fun modI => fun modJ => fun ringR_args => fun ringP_args => forall (Q : Prop), forall (mk : forall (pair_hom : @RingHomLawArgs.{succ u,succ p} R zeroR oneR addR negR subR mulR P zeroP oneP addP negP subP mulP (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ)), forall (kernel_to_intersection : forall (x : R), forall (h : @Eq.{succ p} P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ x) zeroP), @RingCrtIntersectionPred.{succ u,succ v,succ w} R RI RJ zeroI zeroJ modI modJ x), forall (intersection_to_kernel : forall (x : R), forall (h : @RingCrtIntersectionPred.{succ u,succ v,succ w} R RI RJ zeroI zeroJ modI modJ x), @Eq.{succ p} P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ x) zeroP), forall (first_iso_to_image : @RingFirstIso.{u,p} R zeroR oneR addR negR subR mulR P zeroP oneP addP negP subP mulP (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ) ringR_args ringP_args pair_hom), forall (full_product_image : forall (y : P), @RingImagePred.{succ u,succ p} R P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ) y), forall (quot_surj_product : forall (y : P), forall (S : Prop), forall (mk_surj : forall (q : @RingKerQuot.{u,p} R P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ)), forall (h : @Eq.{succ p} P (@RingKerQuotToS.{u,p} R P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ) q) y), S), S), Q), Q