∀ {J : Type u_3} {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] (B : C) (objs : J → C)
  (arrows : (j : J) → B ⟶ objs j) {X Y Z : CategoryTheory.Limits.WidePushoutShape J} (f : X ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.Limits.WidePushoutShape.Hom.casesOn (motive := fun a a_1 x =>
      X = a →
        Z = a_1 → CategoryTheory.CategoryStruct.comp f g ≍ x → (Option.casesOn X B objs ⟶ Option.casesOn Z B objs))
      (CategoryTheory.CategoryStruct.comp f g)
      (fun X_1 h =>
        Eq.ndrec (motive := fun X_2 =>
          Z = X_2 →
            CategoryTheory.CategoryStruct.comp f g ≍ CategoryTheory.Limits.WidePushoutShape.Hom.id X_2 →
              (Option.casesOn X B objs ⟶ Option.casesOn Z B objs))
          (fun h =>
            Eq.ndrec (motive := fun {Y} =>
              (f : X ⟶ Y) →
                f ≍ CategoryTheory.Limits.WidePushoutShape.Hom.id X →
                  (Option.casesOn X B objs ⟶ Option.casesOn Y B objs))
              (fun f h => CategoryTheory.CategoryStruct.id (Option.casesOn X B objs)) ⋯
              (CategoryTheory.CategoryStruct.comp f g))
          h)
      (fun j h =>
        Eq.ndrec (motive := fun {X} =>
          (f : X ⟶ Z) →
            Z = some j →
              f ≍ CategoryTheory.Limits.WidePushoutShape.Hom.init j →
                (Option.casesOn X B objs ⟶ Option.casesOn Z B objs))
          (fun f h =>
            Eq.ndrec (motive := fun {Y} =>
              (f : none ⟶ Y) →
                f ≍ CategoryTheory.Limits.WidePushoutShape.Hom.init j →
                  (Option.casesOn none B objs ⟶ Option.casesOn Y B objs))
              (fun f h => arrows j) ⋯ f)
          ⋯ (CategoryTheory.CategoryStruct.comp f g))
      ⋯ ⋯ ⋯ =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.WidePushoutShape.Hom.casesOn (motive := fun a a_1 x =>
        X = a → Y = a_1 → f ≍ x → (Option.casesOn X B objs ⟶ Option.casesOn Y B objs)) f
        (fun X_1 h =>
          Eq.ndrec (motive := fun X_2 =>
            Y = X_2 →
              f ≍ CategoryTheory.Limits.WidePushoutShape.Hom.id X_2 →
                (Option.casesOn X B objs ⟶ Option.casesOn Y B objs))
            (fun h =>
              Eq.ndrec (motive := fun {Y} =>
                (f : X ⟶ Y) →
                  f ≍ CategoryTheory.Limits.WidePushoutShape.Hom.id X →
                    (Option.casesOn X B objs ⟶ Option.casesOn Y B objs))
                (fun f h => CategoryTheory.CategoryStruct.id (Option.casesOn X B objs)) ⋯ f)
            h)
        (fun j h =>
          Eq.ndrec (motive := fun {X} =>
            (f : X ⟶ Y) →
              Y = some j →
                f ≍ CategoryTheory.Limits.WidePushoutShape.Hom.init j →
                  (Option.casesOn X B objs ⟶ Option.casesOn Y B objs))
            (fun f h =>
              Eq.ndrec (motive := fun {Y} =>
                (f : none ⟶ Y) →
                  f ≍ CategoryTheory.Limits.WidePushoutShape.Hom.init j →
                    (Option.casesOn none B objs ⟶ Option.casesOn Y B objs))
                (fun f h => arrows j) ⋯ f)
            ⋯ f)
        ⋯ ⋯ ⋯)
      (CategoryTheory.Limits.WidePushoutShape.Hom.casesOn (motive := fun a a_1 x =>
        Y = a → Z = a_1 → g ≍ x → (Option.casesOn Y B objs ⟶ Option.casesOn Z B objs)) g
        (fun X h =>
          Eq.ndrec (motive := fun X =>
            Z = X →
              g ≍ CategoryTheory.Limits.WidePushoutShape.Hom.id X → (Option.casesOn Y B objs ⟶ Option.casesOn Z B objs))
            (fun h =>
              Eq.ndrec (motive := fun {Y_1} =>
                (f : Y ⟶ Y_1) →
                  f ≍ CategoryTheory.Limits.WidePushoutShape.Hom.id Y →
                    (Option.casesOn Y B objs ⟶ Option.casesOn Y_1 B objs))
                (fun f h => CategoryTheory.CategoryStruct.id (Option.casesOn Y B objs)) ⋯ g)
            h)
        (fun j h =>
          Eq.ndrec (motive := fun {X} =>
            (f : X ⟶ Z) →
              Z = some j →
                f ≍ CategoryTheory.Limits.WidePushoutShape.Hom.init j →
                  (Option.casesOn X B objs ⟶ Option.casesOn Z B objs))
            (fun f h =>
              Eq.ndrec (motive := fun {Y} =>
                (f : none ⟶ Y) →
                  f ≍ CategoryTheory.Limits.WidePushoutShape.Hom.init j →
                    (Option.casesOn none B objs ⟶ Option.casesOn Y B objs))
                (fun f h => arrows j) ⋯ f)
            ⋯ g)
        ⋯ ⋯ ⋯)