ring_crt_kernel_to_intersection

forall (R : Sort succ u), forall (RI : Sort succ v), forall (RJ : Sort succ w), forall (P : Sort succ p), forall (zeroI : RI), forall (zeroJ : RJ), forall (zeroP : 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 (fst_pair : forall (x : RI), forall (y : RJ), @Eq.{succ v} RI (fst (pair x y)) x), forall (snd_pair : forall (x : RI), forall (y : RJ), @Eq.{succ w} RJ (snd (pair x y)) y), forall (zero_pair : @Eq.{succ p} P (pair zeroI zeroJ) zeroP), 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

theorem ring_crt_kernel_to_intersection.{p,u,v,w} :
  forall (R : Sort succ u), forall (RI : Sort succ v), forall (RJ : Sort succ w), forall (P : Sort succ p), forall (zeroI : RI), forall (zeroJ : RJ), forall (zeroP : 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 (fst_pair : forall (x : RI), forall (y : RJ), @Eq.{succ v} RI (fst (pair x y)) x), forall (snd_pair : forall (x : RI), forall (y : RJ), @Eq.{succ w} RJ (snd (pair x y)) y), forall (zero_pair : @Eq.{succ p} P (pair zeroI zeroJ) zeroP), 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 :=
  fun R => fun RI => fun RJ => fun P => fun zeroI => fun zeroJ => fun zeroP => fun pair => fun fst => fun snd => fun modI => fun modJ => fun fst_pair => fun snd_pair => fun zero_pair => fun x => fun h => @ring_crt_intersection_intro.{succ u,succ v,succ w} R RI RJ zeroI zeroJ modI modJ x (@eq_trans.{succ v} RI (modI x) (fst (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ x)) zeroI (@eq_symm.{succ v} RI (fst (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ x)) (modI x) (fst_pair (modI x) (modJ x))) (@eq_trans.{succ v} RI (fst (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ x)) (fst zeroP) zeroI (@eq_congr_arg.{succ p,succ v} P RI fst (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ x) zeroP h) (@eq_trans.{succ v} RI (fst zeroP) (fst (pair zeroI zeroJ)) zeroI (@eq_symm.{succ v} RI (fst (pair zeroI zeroJ)) (fst zeroP) (@eq_congr_arg.{succ p,succ v} P RI fst (pair zeroI zeroJ) zeroP zero_pair)) (fst_pair zeroI zeroJ)))) (@eq_trans.{succ w} RJ (modJ x) (snd (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ x)) zeroJ (@eq_symm.{succ w} RJ (snd (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ x)) (modJ x) (snd_pair (modI x) (modJ x))) (@eq_trans.{succ w} RJ (snd (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ x)) (snd zeroP) zeroJ (@eq_congr_arg.{succ p,succ w} P RJ snd (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ x) zeroP h) (@eq_trans.{succ w} RJ (snd zeroP) (snd (pair zeroI zeroJ)) zeroJ (@eq_symm.{succ w} RJ (snd (pair zeroI zeroJ)) (snd zeroP) (@eq_congr_arg.{succ p,succ w} P RJ snd (pair zeroI zeroJ) zeroP zero_pair)) (snd_pair zeroI zeroJ))))