-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
⊢ Eq (α :=
    Quiver.Hom (V := WalkingParallelPairᵒᵖ)
      (op
          (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : zero = t) → WalkingParallelPair)
            zero (fun (h : zero = zero) ↦ one) (fun (h : zero = one) ↦ zero) ⋯) :
        WalkingParallelPairᵒᵖ)
      (op
          (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : one = t) → WalkingParallelPair)
            one (fun (h : one = zero) ↦ one) (fun (h : one = one) ↦ zero) ⋯) :
        WalkingParallelPairᵒᵖ))
    (@WalkingParallelPairHom.casesOn
        (fun (a a_1 : WalkingParallelPair) (t : WalkingParallelPairHom a a_1) ↦
          (h : zero = a) →
            (h : one = a_1) →
              (h : HEq (α := zero ⟶ one) (WalkingParallelPairHom.id zero ≫ left) t) →
                Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                  (op
                      (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                        (h : zero = t) → WalkingParallelPair) zero (fun (h : zero = zero) ↦ one)
                        (fun (h : zero = one) ↦ zero) ⋯) :
                    WalkingParallelPairᵒᵖ)
                  (op
                      (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                        (h : one = t) → WalkingParallelPair) one (fun (h : one = zero) ↦ one)
                        (fun (h : one = one) ↦ zero) ⋯) :
                    WalkingParallelPairᵒᵖ))
        zero one (WalkingParallelPairHom.id zero ≫ left)
        (fun (h : zero = zero) ↦
          Eq.ndrec (motive := fun {X : WalkingParallelPair} ↦
            (f : X ⟶ one) →
              (h : one = one) →
                (h : f ≍ left) →
                  Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                    (op
                        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                          (h : X = t) → WalkingParallelPair) X (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero)
                          ⋯) :
                      WalkingParallelPairᵒᵖ)
                    (op
                        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                          (h : one = t) → WalkingParallelPair) one (fun (h : one = zero) ↦ one)
                          (fun (h : one = one) ↦ zero) ⋯) :
                      WalkingParallelPairᵒᵖ))
            (fun (f : zero ⟶ one) (h : one = one) ↦
              Eq.ndrec (motive := fun {Y : WalkingParallelPair} ↦
                (f : zero ⟶ Y) →
                  (h : f ≍ left) →
                    Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                      (op
                          (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                            (h : zero = t) → WalkingParallelPair) zero (fun (h : zero = zero) ↦ one)
                            (fun (h : zero = one) ↦ zero) ⋯) :
                        WalkingParallelPairᵒᵖ)
                      (op
                          (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                            (h : Y = t) → WalkingParallelPair) Y (fun (h : Y = zero) ↦ one) (fun (h : Y = one) ↦ zero)
                            ⋯) :
                        WalkingParallelPairᵒᵖ))
                (fun (f : zero ⟶ one) (h : f ≍ left) ↦ Quiver.Hom.op left) ⋯ f)
            ⋯ (WalkingParallelPairHom.id zero ≫ left))
        (fun (h : zero = zero) ↦
          Eq.ndrec (motive := fun {X : WalkingParallelPair} ↦
            (f : X ⟶ one) →
              (h : one = one) →
                (h : f ≍ right) →
                  Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                    (op
                        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                          (h : X = t) → WalkingParallelPair) X (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero)
                          ⋯) :
                      WalkingParallelPairᵒᵖ)
                    (op
                        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                          (h : one = t) → WalkingParallelPair) one (fun (h : one = zero) ↦ one)
                          (fun (h : one = one) ↦ zero) ⋯) :
                      WalkingParallelPairᵒᵖ))
            (fun (f : zero ⟶ one) (h : one = one) ↦
              Eq.ndrec (motive := fun {Y : WalkingParallelPair} ↦
                (f : zero ⟶ Y) →
                  (h : f ≍ right) →
                    Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                      (op
                          (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                            (h : zero = t) → WalkingParallelPair) zero (fun (h : zero = zero) ↦ one)
                            (fun (h : zero = one) ↦ zero) ⋯) :
                        WalkingParallelPairᵒᵖ)
                      (op
                          (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                            (h : Y = t) → WalkingParallelPair) Y (fun (h : Y = zero) ↦ one) (fun (h : Y = one) ↦ zero)
                            ⋯) :
                        WalkingParallelPairᵒᵖ))
                (fun (f : zero ⟶ one) (h : f ≍ right) ↦ Quiver.Hom.op right) ⋯ f)
            ⋯ (WalkingParallelPairHom.id zero ≫ left))
        (fun (X : WalkingParallelPair) (h : zero = X) ↦
          Eq.ndrec (motive := fun (X : WalkingParallelPair) ↦
            (h : one = X) →
              (h : HEq (α := zero ⟶ one) (WalkingParallelPairHom.id zero ≫ left) (WalkingParallelPairHom.id X)) →
                Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                  (op
                      (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                        (h : zero = t) → WalkingParallelPair) zero (fun (h : zero = zero) ↦ one)
                        (fun (h : zero = one) ↦ zero) ⋯) :
                    WalkingParallelPairᵒᵖ)
                  (op
                      (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                        (h : one = t) → WalkingParallelPair) one (fun (h : one = zero) ↦ one)
                        (fun (h : one = one) ↦ zero) ⋯) :
                    WalkingParallelPairᵒᵖ))
            (fun (h : one = zero) ↦
              Eq.ndrec (motive := fun {Y : WalkingParallelPair} ↦
                (f : zero ⟶ Y) →
                  (h : f ≍ WalkingParallelPairHom.id zero) →
                    Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                      (op
                          (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                            (h : zero = t) → WalkingParallelPair) zero (fun (h : zero = zero) ↦ one)
                            (fun (h : zero = one) ↦ zero) ⋯) :
                        WalkingParallelPairᵒᵖ)
                      (op
                          (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                            (h : Y = t) → WalkingParallelPair) Y (fun (h : Y = zero) ↦ one) (fun (h : Y = one) ↦ zero)
                            ⋯) :
                        WalkingParallelPairᵒᵖ))
                (fun (f : zero ⟶ zero) (h : f ≍ WalkingParallelPairHom.id zero) ↦
                  Quiver.Hom.op
                    (WalkingParallelPairHom.id
                      (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                        (h : zero = t) → WalkingParallelPair) zero (fun (h : zero = zero) ↦ one)
                        (fun (h : zero = one) ↦ zero) ⋯)))
                ⋯ (WalkingParallelPairHom.id zero ≫ left))
            h)
        ⋯ ⋯ ⋯ :
      Quiver.Hom (V := WalkingParallelPairᵒᵖ)
        (op
            (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
              (h : zero = t) → WalkingParallelPair) zero (fun (h : zero = zero) ↦ one) (fun (h : zero = one) ↦ zero)
              ⋯) :
          WalkingParallelPairᵒᵖ)
        (op
            (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : one = t) → WalkingParallelPair)
              one (fun (h : one = zero) ↦ one) (fun (h : one = one) ↦ zero) ⋯) :
          WalkingParallelPairᵒᵖ))
    (CategoryStruct.comp (Y :=
        op
          (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : zero = t) → WalkingParallelPair)
            zero (fun (h : zero = zero) ↦ one) (fun (h : zero = one) ↦ zero) ⋯))
        (WalkingParallelPairHom.casesOn (motive :=
          fun (a a_1 : WalkingParallelPair) (t : WalkingParallelPairHom a a_1) ↦
          (h : zero = a) →
            (h : zero = a_1) →
              (h : WalkingParallelPairHom.id zero ≍ t) →
                Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                  (op
                      (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                        (h : zero = t) → WalkingParallelPair) zero (fun (h : zero = zero) ↦ one)
                        (fun (h : zero = one) ↦ zero) ⋯) :
                    WalkingParallelPairᵒᵖ)
                  (op
                      (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                        (h : zero = t) → WalkingParallelPair) zero (fun (h : zero = zero) ↦ one)
                        (fun (h : zero = one) ↦ zero) ⋯) :
                    WalkingParallelPairᵒᵖ))
          (WalkingParallelPairHom.id zero)
          (fun (h : zero = zero) ↦
            Eq.ndrec (motive := fun {X : WalkingParallelPair} ↦
              (f : X ⟶ zero) →
                (h : zero = one) →
                  (h : f ≍ left) →
                    Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                      (op
                          (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                            (h : X = t) → WalkingParallelPair) X (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero)
                            ⋯) :
                        WalkingParallelPairᵒᵖ)
                      (op
                          (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                            (h : zero = t) → WalkingParallelPair) zero (fun (h : zero = zero) ↦ one)
                            (fun (h : zero = one) ↦ zero) ⋯) :
                        WalkingParallelPairᵒᵖ))
              (fun (f : zero ⟶ zero) (h : zero = one) ↦
                Eq.ndrec (motive := fun {Y : WalkingParallelPair} ↦
                  (f : zero ⟶ Y) →
                    (h : f ≍ left) →
                      Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                        (op
                            (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                              (h : zero = t) → WalkingParallelPair) zero (fun (h : zero = zero) ↦ one)
                              (fun (h : zero = one) ↦ zero) ⋯) :
                          WalkingParallelPairᵒᵖ)
                        (op
                            (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                              (h : Y = t) → WalkingParallelPair) Y (fun (h : Y = zero) ↦ one) (fun (h : Y = one) ↦ zero)
                              ⋯) :
                          WalkingParallelPairᵒᵖ))
                  (fun (f : zero ⟶ one) (h : f ≍ left) ↦ Quiver.Hom.op left) ⋯ f)
              ⋯ (WalkingParallelPairHom.id zero))
          (fun (h : zero = zero) ↦
            Eq.ndrec (motive := fun {X : WalkingParallelPair} ↦
              (f : X ⟶ zero) →
                (h : zero = one) →
                  (h : f ≍ right) →
                    Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                      (op
                          (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                            (h : X = t) → WalkingParallelPair) X (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero)
                            ⋯) :
                        WalkingParallelPairᵒᵖ)
                      (op
                          (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                            (h : zero = t) → WalkingParallelPair) zero (fun (h : zero = zero) ↦ one)
                            (fun (h : zero = one) ↦ zero) ⋯) :
                        WalkingParallelPairᵒᵖ))
              (fun (f : zero ⟶ zero) (h : zero = one) ↦
                Eq.ndrec (motive := fun {Y : WalkingParallelPair} ↦
                  (f : zero ⟶ Y) →
                    (h : f ≍ right) →
                      Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                        (op
                            (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                              (h : zero = t) → WalkingParallelPair) zero (fun (h : zero = zero) ↦ one)
                              (fun (h : zero = one) ↦ zero) ⋯) :
                          WalkingParallelPairᵒᵖ)
                        (op
                            (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                              (h : Y = t) → WalkingParallelPair) Y (fun (h : Y = zero) ↦ one) (fun (h : Y = one) ↦ zero)
                              ⋯) :
                          WalkingParallelPairᵒᵖ))
                  (fun (f : zero ⟶ one) (h : f ≍ right) ↦ Quiver.Hom.op right) ⋯ f)
              ⋯ (WalkingParallelPairHom.id zero))
          (fun (X : WalkingParallelPair) (h : zero = X) ↦
            Eq.ndrec (motive := fun (X : WalkingParallelPair) ↦
              (h : zero = X) →
                (h : WalkingParallelPairHom.id zero ≍ WalkingParallelPairHom.id X) →
                  Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                    (op
                        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                          (h : zero = t) → WalkingParallelPair) zero (fun (h : zero = zero) ↦ one)
                          (fun (h : zero = one) ↦ zero) ⋯) :
                      WalkingParallelPairᵒᵖ)
                    (op
                        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                          (h : zero = t) → WalkingParallelPair) zero (fun (h : zero = zero) ↦ one)
                          (fun (h : zero = one) ↦ zero) ⋯) :
                      WalkingParallelPairᵒᵖ))
              (fun (h : zero = zero) ↦
                Eq.ndrec (motive := fun {Y : WalkingParallelPair} ↦
                  (f : zero ⟶ Y) →
                    (h : f ≍ WalkingParallelPairHom.id zero) →
                      Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                        (op
                            (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                              (h : zero = t) → WalkingParallelPair) zero (fun (h : zero = zero) ↦ one)
                              (fun (h : zero = one) ↦ zero) ⋯) :
                          WalkingParallelPairᵒᵖ)
                        (op
                            (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                              (h : Y = t) → WalkingParallelPair) Y (fun (h : Y = zero) ↦ one) (fun (h : Y = one) ↦ zero)
                              ⋯) :
                          WalkingParallelPairᵒᵖ))
                  (fun (f : zero ⟶ zero) (h : f ≍ WalkingParallelPairHom.id zero) ↦
                    Quiver.Hom.op
                      (WalkingParallelPairHom.id
                        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                          (h : zero = t) → WalkingParallelPair) zero (fun (h : zero = zero) ↦ one)
                          (fun (h : zero = one) ↦ zero) ⋯)))
                  ⋯ (WalkingParallelPairHom.id zero))
              h)
          ⋯ ⋯ ⋯)
        (WalkingParallelPairHom.casesOn (motive :=
          fun (a a_1 : WalkingParallelPair) (t : WalkingParallelPairHom a a_1) ↦
          (h : zero = a) →
            (h : one = a_1) →
              (h : left ≍ t) →
                Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                  (op
                      (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                        (h : zero = t) → WalkingParallelPair) zero (fun (h : zero = zero) ↦ one)
                        (fun (h : zero = one) ↦ zero) ⋯) :
                    WalkingParallelPairᵒᵖ)
                  (op
                      (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                        (h : one = t) → WalkingParallelPair) one (fun (h : one = zero) ↦ one)
                        (fun (h : one = one) ↦ zero) ⋯) :
                    WalkingParallelPairᵒᵖ))
          left
          (fun (h : zero = zero) ↦
            Eq.ndrec (motive := fun {X : WalkingParallelPair} ↦
              (f : X ⟶ one) →
                (h : one = one) →
                  (h : f ≍ left) →
                    Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                      (op
                          (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                            (h : X = t) → WalkingParallelPair) X (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero)
                            ⋯) :
                        WalkingParallelPairᵒᵖ)
                      (op
                          (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                            (h : one = t) → WalkingParallelPair) one (fun (h : one = zero) ↦ one)
                            (fun (h : one = one) ↦ zero) ⋯) :
                        WalkingParallelPairᵒᵖ))
              (fun (f : zero ⟶ one) (h : one = one) ↦
                Eq.ndrec (motive := fun {Y : WalkingParallelPair} ↦
                  (f : zero ⟶ Y) →
                    (h : f ≍ left) →
                      Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                        (op
                            (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                              (h : zero = t) → WalkingParallelPair) zero (fun (h : zero = zero) ↦ one)
                              (fun (h : zero = one) ↦ zero) ⋯) :
                          WalkingParallelPairᵒᵖ)
                        (op
                            (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                              (h : Y = t) → WalkingParallelPair) Y (fun (h : Y = zero) ↦ one) (fun (h : Y = one) ↦ zero)
                              ⋯) :
                          WalkingParallelPairᵒᵖ))
                  (fun (f : zero ⟶ one) (h : f ≍ left) ↦ Quiver.Hom.op left) ⋯ f)
              ⋯ left)
          (fun (h : zero = zero) ↦
            Eq.ndrec (motive := fun {X : WalkingParallelPair} ↦
              (f : X ⟶ one) →
                (h : one = one) →
                  (h : f ≍ right) →
                    Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                      (op
                          (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                            (h : X = t) → WalkingParallelPair) X (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero)
                            ⋯) :
                        WalkingParallelPairᵒᵖ)
                      (op
                          (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                            (h : one = t) → WalkingParallelPair) one (fun (h : one = zero) ↦ one)
                            (fun (h : one = one) ↦ zero) ⋯) :
                        WalkingParallelPairᵒᵖ))
              (fun (f : zero ⟶ one) (h : one = one) ↦
                Eq.ndrec (motive := fun {Y : WalkingParallelPair} ↦
                  (f : zero ⟶ Y) →
                    (h : f ≍ right) →
                      Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                        (op
                            (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                              (h : zero = t) → WalkingParallelPair) zero (fun (h : zero = zero) ↦ one)
                              (fun (h : zero = one) ↦ zero) ⋯) :
                          WalkingParallelPairᵒᵖ)
                        (op
                            (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                              (h : Y = t) → WalkingParallelPair) Y (fun (h : Y = zero) ↦ one) (fun (h : Y = one) ↦ zero)
                              ⋯) :
                          WalkingParallelPairᵒᵖ))
                  (fun (f : zero ⟶ one) (h : f ≍ right) ↦ Quiver.Hom.op right) ⋯ f)
              ⋯ left)
          (fun (X : WalkingParallelPair) (h : zero = X) ↦
            Eq.ndrec (motive := fun (X : WalkingParallelPair) ↦
              (h : one = X) →
                (h : left ≍ WalkingParallelPairHom.id X) →
                  Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                    (op
                        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                          (h : zero = t) → WalkingParallelPair) zero (fun (h : zero = zero) ↦ one)
                          (fun (h : zero = one) ↦ zero) ⋯) :
                      WalkingParallelPairᵒᵖ)
                    (op
                        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                          (h : one = t) → WalkingParallelPair) one (fun (h : one = zero) ↦ one)
                          (fun (h : one = one) ↦ zero) ⋯) :
                      WalkingParallelPairᵒᵖ))
              (fun (h : one = zero) ↦
                Eq.ndrec (motive := fun {Y : WalkingParallelPair} ↦
                  (f : zero ⟶ Y) →
                    (h : f ≍ WalkingParallelPairHom.id zero) →
                      Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                        (op
                            (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                              (h : zero = t) → WalkingParallelPair) zero (fun (h : zero = zero) ↦ one)
                              (fun (h : zero = one) ↦ zero) ⋯) :
                          WalkingParallelPairᵒᵖ)
                        (op
                            (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                              (h : Y = t) → WalkingParallelPair) Y (fun (h : Y = zero) ↦ one) (fun (h : Y = one) ↦ zero)
                              ⋯) :
                          WalkingParallelPairᵒᵖ))
                  (fun (f : zero ⟶ zero) (h : f ≍ WalkingParallelPairHom.id zero) ↦
                    Quiver.Hom.op
                      (WalkingParallelPairHom.id
                        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                          (h : zero = t) → WalkingParallelPair) zero (fun (h : zero = zero) ↦ one)
                          (fun (h : zero = one) ↦ zero) ⋯)))
                  ⋯ left)
              h)
          ⋯ ⋯ ⋯) :
      Quiver.Hom (V := WalkingParallelPairᵒᵖ)
        (op
            (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
              (h : zero = t) → WalkingParallelPair) zero (fun (h : zero = zero) ↦ one) (fun (h : zero = one) ↦ zero)
              ⋯) :
          WalkingParallelPairᵒᵖ)
        (op
            (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : one = t) → WalkingParallelPair)
              one (fun (h : one = zero) ↦ one) (fun (h : one = one) ↦ zero) ⋯) :
          WalkingParallelPairᵒᵖ))

Tactic:
rfl