{X : SSet.Truncated 2} →
  {x₀ x₁ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := SSet.Truncated.Edge._proof_1 })} →
    {motive : SSet.Truncated.Edge x₀ x₁ → Sort u_1} →
      (t : SSet.Truncated.Edge x₀ x₁) →
        ((edge : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := SSet.Truncated.Edge._proof_2 })) →
            (src_eq :
                X.map (SimplexCategory.Truncated.δ₂ 1 SSet.Truncated.Edge._proof_1 SSet.Truncated.Edge._proof_3).op
                    edge =
                  x₀) →
              (tgt_eq :
                  X.map (SimplexCategory.Truncated.δ₂ 0 SSet.Truncated.Edge._proof_1 SSet.Truncated.Edge._proof_3).op
                      edge =
                    x₁) →
                motive { edge := edge, src_eq := src_eq, tgt_eq := tgt_eq }) →
          motive t