∀ {X Y : SSet.Truncated 2}
  (f₀ :
    X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_11✝ }) →
      Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := _proof_11✝¹ }))
  (f₁ :
    X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝ }) →
      Y.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝¹ })),
  (∀ (x : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝² })),
      f₀ (X.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝² _proof_13✝).op x) =
        Y.map (SimplexCategory.Truncated.δ₂ 1 _proof_11✝³ _proof_13✝¹).op (f₁ x)) →
    (∀ (x : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := _proof_12✝³ })),
        f₀ (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝⁴ _proof_13✝²).op x) =
          Y.map (SimplexCategory.Truncated.δ₂ 0 _proof_11✝⁵ _proof_13✝³).op (f₁ x)) →
      ∀ (x : X.obj (Opposite.op { obj := SimplexCategory.mk 2, property := _proof_14✝ })),
        (Y.spine 1 SSet.Truncated.liftOfStrictSegal.f₂._proof_6
                (f₁ (X.map (SimplexCategory.Truncated.δ₂ 2 _proof_12✝⁴ _proof_15✝).op x))).vertex
            1 =
          (Y.spine 1 SSet.Truncated.liftOfStrictSegal.f₂._proof_6
                (f₁ (X.map (SimplexCategory.Truncated.δ₂ 0 _proof_12✝⁵ _proof_15✝¹).op x))).vertex
            0