-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
Z : WalkingParallelPair
g : one ⟶ Z
⊢ 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 : Z = t) → WalkingParallelPair) Z
            (fun (h : Z = zero) ↦ one) (fun (h : Z = one) ↦ zero) ⋯) :
        WalkingParallelPairᵒᵖ))
    (@WalkingParallelPairHom.casesOn
        (fun (a a_1 : WalkingParallelPair) (t : WalkingParallelPairHom a a_1) ↦
          (h : zero = a) →
            (h : Z = a_1) →
              (h : HEq (α := zero ⟶ Z) (right ≫ g) 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 : Z = t) → WalkingParallelPair) Z (fun (h : Z = zero) ↦ one) (fun (h : Z = one) ↦ zero) ⋯) :
                    WalkingParallelPairᵒᵖ))
        zero _ (right ≫ g)
        (fun (h : zero = zero) ↦
          Eq.ndrec (motive := fun {X : WalkingParallelPair} ↦
            (f : X ⟶ Z) →
              (h : Z = 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 : Z = t) → WalkingParallelPair) Z (fun (h : Z = zero) ↦ one) (fun (h : Z = one) ↦ zero)
                          ⋯) :
                      WalkingParallelPairᵒᵖ))
            (fun (f : zero ⟶ Z) (h : Z = 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)
            ⋯ (right ≫ g))
        (fun (h : zero = zero) ↦
          Eq.ndrec (motive := fun {X : WalkingParallelPair} ↦
            (f : X ⟶ Z) →
              (h : Z = 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 : Z = t) → WalkingParallelPair) Z (fun (h : Z = zero) ↦ one) (fun (h : Z = one) ↦ zero)
                          ⋯) :
                      WalkingParallelPairᵒᵖ))
            (fun (f : zero ⟶ Z) (h : Z = 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)
            ⋯ (right ≫ g))
        (fun (X : WalkingParallelPair) (h : zero = X) ↦
          Eq.ndrec (motive := fun (X : WalkingParallelPair) ↦
            (h : Z = X) →
              (h : HEq (α := zero ⟶ Z) (right ≫ g) (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 : Z = t) → WalkingParallelPair) Z (fun (h : Z = zero) ↦ one) (fun (h : Z = one) ↦ zero) ⋯) :
                    WalkingParallelPairᵒᵖ))
            (fun (h : Z = 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) ⋯)))
                ⋯ (right ≫ g))
            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 : Z = t) → WalkingParallelPair) Z
              (fun (h : Z = zero) ↦ one) (fun (h : Z = one) ↦ zero) ⋯) :
          WalkingParallelPairᵒᵖ))
    (CategoryStruct.comp (Y :=
        op
          (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : one = t) → WalkingParallelPair)
            one (fun (h : one = zero) ↦ one) (fun (h : one = one) ↦ zero) ⋯))
        (WalkingParallelPairHom.casesOn (motive :=
          fun (a a_1 : WalkingParallelPair) (t : WalkingParallelPairHom a a_1) ↦
          (h : zero = a) →
            (h : one = a_1) →
              (h : right ≍ 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ᵒᵖ))
          right
          (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)
              ⋯ right)
          (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)
              ⋯ right)
          (fun (X : WalkingParallelPair) (h : zero = X) ↦
            Eq.ndrec (motive := fun (X : WalkingParallelPair) ↦
              (h : one = X) →
                (h : right ≍ 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) ⋯)))
                  ⋯ right)
              h)
          ⋯ ⋯ ⋯)
        (WalkingParallelPairHom.casesOn (motive :=
          fun (a a_1 : WalkingParallelPair) (t : WalkingParallelPairHom a a_1) ↦
          (h : one = a) →
            (h : Z = a_1) →
              (h : g ≍ t) →
                Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                  (op
                      (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                        (h : one = t) → WalkingParallelPair) one (fun (h : one = zero) ↦ one)
                        (fun (h : one = one) ↦ zero) ⋯) :
                    WalkingParallelPairᵒᵖ)
                  (op
                      (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                        (h : Z = t) → WalkingParallelPair) Z (fun (h : Z = zero) ↦ one) (fun (h : Z = one) ↦ zero) ⋯) :
                    WalkingParallelPairᵒᵖ))
          g
          (fun (h : one = zero) ↦
            Eq.ndrec (motive := fun {X : WalkingParallelPair} ↦
              (f : X ⟶ Z) →
                (h : Z = 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 : Z = t) → WalkingParallelPair) Z (fun (h : Z = zero) ↦ one) (fun (h : Z = one) ↦ zero)
                            ⋯) :
                        WalkingParallelPairᵒᵖ))
              (fun (f : zero ⟶ Z) (h : Z = 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)
              ⋯ g)
          (fun (h : one = zero) ↦
            Eq.ndrec (motive := fun {X : WalkingParallelPair} ↦
              (f : X ⟶ Z) →
                (h : Z = 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 : Z = t) → WalkingParallelPair) Z (fun (h : Z = zero) ↦ one) (fun (h : Z = one) ↦ zero)
                            ⋯) :
                        WalkingParallelPairᵒᵖ))
              (fun (f : zero ⟶ Z) (h : Z = 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)
              ⋯ g)
          (fun (X : WalkingParallelPair) (h : one = X) ↦
            Eq.ndrec (motive := fun (X : WalkingParallelPair) ↦
              (h : Z = X) →
                (h : g ≍ WalkingParallelPairHom.id X) →
                  Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                    (op
                        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                          (h : one = t) → WalkingParallelPair) one (fun (h : one = zero) ↦ one)
                          (fun (h : one = one) ↦ zero) ⋯) :
                      WalkingParallelPairᵒᵖ)
                    (op
                        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                          (h : Z = t) → WalkingParallelPair) Z (fun (h : Z = zero) ↦ one) (fun (h : Z = one) ↦ zero)
                          ⋯) :
                      WalkingParallelPairᵒᵖ))
              (fun (h : Z = one) ↦
                Eq.ndrec (motive := fun {Y : WalkingParallelPair} ↦
                  (f : one ⟶ Y) →
                    (h : f ≍ WalkingParallelPairHom.id one) →
                      Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                        (op
                            (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                              (h : one = t) → WalkingParallelPair) one (fun (h : one = zero) ↦ one)
                              (fun (h : one = 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 : one ⟶ one) (h : f ≍ WalkingParallelPairHom.id one) ↦
                    Quiver.Hom.op
                      (WalkingParallelPairHom.id
                        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                          (h : one = t) → WalkingParallelPair) one (fun (h : one = zero) ↦ one)
                          (fun (h : one = one) ↦ zero) ⋯)))
                  ⋯ g)
              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 : Z = t) → WalkingParallelPair) Z
              (fun (h : Z = zero) ↦ one) (fun (h : Z = one) ↦ zero) ⋯) :
          WalkingParallelPairᵒᵖ))
have right : 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) sorry) :
      WalkingParallelPairᵒᵖ)
    (op
        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : one = t) → WalkingParallelPair) one
          (fun (h : one = zero) ↦ one) (fun (h : one = one) ↦ zero) sorry) :
      WalkingParallelPairᵒᵖ))
  (@WalkingParallelPairHom.casesOn
      (fun (a a_1 : WalkingParallelPair) (t : WalkingParallelPairHom a a_1) ↦
        (h : zero = a) →
          (h : one = a_1) →
            (h : HEq (α := zero ⟶ one) (right ≫ WalkingParallelPairHom.id one) 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) sorry) :
                  WalkingParallelPairᵒᵖ)
                (op
                    (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                      (h : one = t) → WalkingParallelPair) one (fun (h : one = zero) ↦ one) (fun (h : one = one) ↦ zero)
                      sorry) :
                  WalkingParallelPairᵒᵖ))
      zero one (right ≫ WalkingParallelPairHom.id one)
      (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) sorry) :
                    WalkingParallelPairᵒᵖ)
                  (op
                      (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                        (h : one = t) → WalkingParallelPair) one (fun (h : one = zero) ↦ one)
                        (fun (h : one = one) ↦ zero) sorry) :
                    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) sorry) :
                      WalkingParallelPairᵒᵖ)
                    (op
                        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                          (h : Y = t) → WalkingParallelPair) Y (fun (h : Y = zero) ↦ one) (fun (h : Y = one) ↦ zero)
                          sorry) :
                      WalkingParallelPairᵒᵖ))
              (fun (f : zero ⟶ one) (h : f ≍ left) ↦ Quiver.Hom.op left) sorry f)
          sorry (right ≫ WalkingParallelPairHom.id one))
      (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) sorry) :
                    WalkingParallelPairᵒᵖ)
                  (op
                      (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                        (h : one = t) → WalkingParallelPair) one (fun (h : one = zero) ↦ one)
                        (fun (h : one = one) ↦ zero) sorry) :
                    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) sorry) :
                      WalkingParallelPairᵒᵖ)
                    (op
                        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                          (h : Y = t) → WalkingParallelPair) Y (fun (h : Y = zero) ↦ one) (fun (h : Y = one) ↦ zero)
                          sorry) :
                      WalkingParallelPairᵒᵖ))
              (fun (f : zero ⟶ one) (h : f ≍ right) ↦ Quiver.Hom.op right) sorry f)
          sorry (right ≫ WalkingParallelPairHom.id one))
      (fun (X : WalkingParallelPair) (h : zero = X) ↦
        Eq.ndrec (motive := fun (X : WalkingParallelPair) ↦
          (h : one = X) →
            (h : HEq (α := zero ⟶ one) (right ≫ WalkingParallelPairHom.id one) (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) sorry) :
                  WalkingParallelPairᵒᵖ)
                (op
                    (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                      (h : one = t) → WalkingParallelPair) one (fun (h : one = zero) ↦ one) (fun (h : one = one) ↦ zero)
                      sorry) :
                  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) sorry) :
                      WalkingParallelPairᵒᵖ)
                    (op
                        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                          (h : Y = t) → WalkingParallelPair) Y (fun (h : Y = zero) ↦ one) (fun (h : Y = one) ↦ zero)
                          sorry) :
                      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) sorry)))
              sorry (right ≫ WalkingParallelPairHom.id one))
          h)
      sorry sorry sorry :
    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) sorry) :
        WalkingParallelPairᵒᵖ)
      (op
          (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : one = t) → WalkingParallelPair)
            one (fun (h : one = zero) ↦ one) (fun (h : one = one) ↦ zero) sorry) :
        WalkingParallelPairᵒᵖ))
  (CategoryStruct.comp (Y :=
      op
        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : one = t) → WalkingParallelPair) one
          (fun (h : one = zero) ↦ one) (fun (h : one = one) ↦ zero) sorry))
      (WalkingParallelPairHom.casesOn (motive := fun (a a_1 : WalkingParallelPair) (t : WalkingParallelPairHom a a_1) ↦
        (h : zero = a) →
          (h : one = a_1) →
            (h : right ≍ 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) sorry) :
                  WalkingParallelPairᵒᵖ)
                (op
                    (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                      (h : one = t) → WalkingParallelPair) one (fun (h : one = zero) ↦ one) (fun (h : one = one) ↦ zero)
                      sorry) :
                  WalkingParallelPairᵒᵖ))
        right
        (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)
                          sorry) :
                      WalkingParallelPairᵒᵖ)
                    (op
                        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                          (h : one = t) → WalkingParallelPair) one (fun (h : one = zero) ↦ one)
                          (fun (h : one = one) ↦ zero) sorry) :
                      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) sorry) :
                        WalkingParallelPairᵒᵖ)
                      (op
                          (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                            (h : Y = t) → WalkingParallelPair) Y (fun (h : Y = zero) ↦ one) (fun (h : Y = one) ↦ zero)
                            sorry) :
                        WalkingParallelPairᵒᵖ))
                (fun (f : zero ⟶ one) (h : f ≍ left) ↦ Quiver.Hom.op left) sorry f)
            sorry right)
        (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)
                          sorry) :
                      WalkingParallelPairᵒᵖ)
                    (op
                        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                          (h : one = t) → WalkingParallelPair) one (fun (h : one = zero) ↦ one)
                          (fun (h : one = one) ↦ zero) sorry) :
                      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) sorry) :
                        WalkingParallelPairᵒᵖ)
                      (op
                          (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                            (h : Y = t) → WalkingParallelPair) Y (fun (h : Y = zero) ↦ one) (fun (h : Y = one) ↦ zero)
                            sorry) :
                        WalkingParallelPairᵒᵖ))
                (fun (f : zero ⟶ one) (h : f ≍ right) ↦ Quiver.Hom.op right) sorry f)
            sorry right)
        (fun (X : WalkingParallelPair) (h : zero = X) ↦
          Eq.ndrec (motive := fun (X : WalkingParallelPair) ↦
            (h : one = X) →
              (h : right ≍ 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) sorry) :
                    WalkingParallelPairᵒᵖ)
                  (op
                      (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                        (h : one = t) → WalkingParallelPair) one (fun (h : one = zero) ↦ one)
                        (fun (h : one = one) ↦ zero) sorry) :
                    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) sorry) :
                        WalkingParallelPairᵒᵖ)
                      (op
                          (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                            (h : Y = t) → WalkingParallelPair) Y (fun (h : Y = zero) ↦ one) (fun (h : Y = one) ↦ zero)
                            sorry) :
                        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) sorry)))
                sorry right)
            h)
        sorry sorry sorry)
      (WalkingParallelPairHom.casesOn (motive := fun (a a_1 : WalkingParallelPair) (t : WalkingParallelPairHom a a_1) ↦
        (h : one = a) →
          (h : one = a_1) →
            (h : WalkingParallelPairHom.id one ≍ t) →
              Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                (op
                    (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                      (h : one = t) → WalkingParallelPair) one (fun (h : one = zero) ↦ one) (fun (h : one = one) ↦ zero)
                      sorry) :
                  WalkingParallelPairᵒᵖ)
                (op
                    (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                      (h : one = t) → WalkingParallelPair) one (fun (h : one = zero) ↦ one) (fun (h : one = one) ↦ zero)
                      sorry) :
                  WalkingParallelPairᵒᵖ))
        (WalkingParallelPairHom.id one)
        (fun (h : one = 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)
                          sorry) :
                      WalkingParallelPairᵒᵖ)
                    (op
                        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                          (h : one = t) → WalkingParallelPair) one (fun (h : one = zero) ↦ one)
                          (fun (h : one = one) ↦ zero) sorry) :
                      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) sorry) :
                        WalkingParallelPairᵒᵖ)
                      (op
                          (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                            (h : Y = t) → WalkingParallelPair) Y (fun (h : Y = zero) ↦ one) (fun (h : Y = one) ↦ zero)
                            sorry) :
                        WalkingParallelPairᵒᵖ))
                (fun (f : zero ⟶ one) (h : f ≍ left) ↦ Quiver.Hom.op left) sorry f)
            sorry (WalkingParallelPairHom.id one))
        (fun (h : one = 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)
                          sorry) :
                      WalkingParallelPairᵒᵖ)
                    (op
                        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                          (h : one = t) → WalkingParallelPair) one (fun (h : one = zero) ↦ one)
                          (fun (h : one = one) ↦ zero) sorry) :
                      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) sorry) :
                        WalkingParallelPairᵒᵖ)
                      (op
                          (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                            (h : Y = t) → WalkingParallelPair) Y (fun (h : Y = zero) ↦ one) (fun (h : Y = one) ↦ zero)
                            sorry) :
                        WalkingParallelPairᵒᵖ))
                (fun (f : zero ⟶ one) (h : f ≍ right) ↦ Quiver.Hom.op right) sorry f)
            sorry (WalkingParallelPairHom.id one))
        (fun (X : WalkingParallelPair) (h : one = X) ↦
          Eq.ndrec (motive := fun (X : WalkingParallelPair) ↦
            (h : one = X) →
              (h : WalkingParallelPairHom.id one ≍ WalkingParallelPairHom.id X) →
                Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                  (op
                      (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                        (h : one = t) → WalkingParallelPair) one (fun (h : one = zero) ↦ one)
                        (fun (h : one = one) ↦ zero) sorry) :
                    WalkingParallelPairᵒᵖ)
                  (op
                      (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                        (h : one = t) → WalkingParallelPair) one (fun (h : one = zero) ↦ one)
                        (fun (h : one = one) ↦ zero) sorry) :
                    WalkingParallelPairᵒᵖ))
            (fun (h : one = one) ↦
              Eq.ndrec (motive := fun {Y : WalkingParallelPair} ↦
                (f : one ⟶ Y) →
                  (h : f ≍ WalkingParallelPairHom.id one) →
                    Quiver.Hom (V := WalkingParallelPairᵒᵖ)
                      (op
                          (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                            (h : one = t) → WalkingParallelPair) one (fun (h : one = zero) ↦ one)
                            (fun (h : one = one) ↦ zero) sorry) :
                        WalkingParallelPairᵒᵖ)
                      (op
                          (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                            (h : Y = t) → WalkingParallelPair) Y (fun (h : Y = zero) ↦ one) (fun (h : Y = one) ↦ zero)
                            sorry) :
                        WalkingParallelPairᵒᵖ))
                (fun (f : one ⟶ one) (h : f ≍ WalkingParallelPairHom.id one) ↦
                  Quiver.Hom.op
                    (WalkingParallelPairHom.id
                      (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦
                        (h : one = t) → WalkingParallelPair) one (fun (h : one = zero) ↦ one)
                        (fun (h : one = one) ↦ zero) sorry)))
                sorry (WalkingParallelPairHom.id one))
            h)
        sorry sorry sorry) :
    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) sorry) :
        WalkingParallelPairᵒᵖ)
      (op
          (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : one = t) → WalkingParallelPair)
            one (fun (h : one = zero) ↦ one) (fun (h : one = one) ↦ zero) sorry) :
        WalkingParallelPairᵒᵖ))
Tactic: cases g
Cleared hypotheses: Z, g