Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case left.reflexion.left
⊢ (Hom.left.comp Hom.reflexion).comp Hom.left = Hom.left.comp (Hom.reflexion.comp Hom.left)

pp: case left.reflexion.right
⊢ (Hom.left.comp Hom.reflexion).comp Hom.right = Hom.left.comp (Hom.reflexion.comp Hom.right)

pp: case left.reflexion.leftCompReflexion
⊢ (Hom.left.comp Hom.reflexion).comp Hom.leftCompReflexion = Hom.left.comp (Hom.reflexion.comp Hom.leftCompReflexion)

pp: case left.reflexion.rightCompReflexion
⊢ (Hom.left.comp Hom.reflexion).comp Hom.rightCompReflexion = Hom.left.comp (Hom.reflexion.comp Hom.rightCompReflexion)

pp: case left.reflexion.id
⊢ (Hom.left.comp Hom.reflexion).comp (Hom.id one) = Hom.left.comp (Hom.reflexion.comp (Hom.id one))

pp: case left.id.reflexion
⊢ (Hom.left.comp (Hom.id zero)).comp Hom.reflexion = Hom.left.comp ((Hom.id zero).comp Hom.reflexion)

pp: case left.id.id
⊢ (Hom.left.comp (Hom.id zero)).comp (Hom.id zero) = Hom.left.comp ((Hom.id zero).comp (Hom.id zero))

pp: case right.reflexion.left
⊢ (Hom.right.comp Hom.reflexion).comp Hom.left = Hom.right.comp (Hom.reflexion.comp Hom.left)

pp: case right.reflexion.right
⊢ (Hom.right.comp Hom.reflexion).comp Hom.right = Hom.right.comp (Hom.reflexion.comp Hom.right)

pp: case right.reflexion.leftCompReflexion
⊢ (Hom.right.comp Hom.reflexion).comp Hom.leftCompReflexion = Hom.right.comp (Hom.reflexion.comp Hom.leftCompReflexion)

pp: case right.reflexion.rightCompReflexion
⊢ (Hom.right.comp Hom.reflexion).comp Hom.rightCompReflexion =
    Hom.right.comp (Hom.reflexion.comp Hom.rightCompReflexion)

pp: case right.reflexion.id
⊢ (Hom.right.comp Hom.reflexion).comp (Hom.id one) = Hom.right.comp (Hom.reflexion.comp (Hom.id one))

pp: case right.id.reflexion
⊢ (Hom.right.comp (Hom.id zero)).comp Hom.reflexion = Hom.right.comp ((Hom.id zero).comp Hom.reflexion)

pp: case right.id.id
⊢ (Hom.right.comp (Hom.id zero)).comp (Hom.id zero) = Hom.right.comp ((Hom.id zero).comp (Hom.id zero))

pp: case reflexion.left.reflexion
⊢ (Hom.reflexion.comp Hom.left).comp Hom.reflexion = Hom.reflexion.comp (Hom.left.comp Hom.reflexion)

pp: case reflexion.left.id
⊢ (Hom.reflexion.comp Hom.left).comp (Hom.id zero) = Hom.reflexion.comp (Hom.left.comp (Hom.id zero))

pp: case reflexion.right.reflexion
⊢ (Hom.reflexion.comp Hom.right).comp Hom.reflexion = Hom.reflexion.comp (Hom.right.comp Hom.reflexion)

pp: case reflexion.right.id
⊢ (Hom.reflexion.comp Hom.right).comp (Hom.id zero) = Hom.reflexion.comp (Hom.right.comp (Hom.id zero))

pp: case reflexion.leftCompReflexion.left
⊢ (Hom.reflexion.comp Hom.leftCompReflexion).comp Hom.left = Hom.reflexion.comp (Hom.leftCompReflexion.comp Hom.left)

pp: case reflexion.leftCompReflexion.right
⊢ (Hom.reflexion.comp Hom.leftCompReflexion).comp Hom.right = Hom.reflexion.comp (Hom.leftCompReflexion.comp Hom.right)

pp: case reflexion.leftCompReflexion.leftCompReflexion
⊢ (Hom.reflexion.comp Hom.leftCompReflexion).comp Hom.leftCompReflexion =
    Hom.reflexion.comp (Hom.leftCompReflexion.comp Hom.leftCompReflexion)

pp: case reflexion.leftCompReflexion.rightCompReflexion
⊢ (Hom.reflexion.comp Hom.leftCompReflexion).comp Hom.rightCompReflexion =
    Hom.reflexion.comp (Hom.leftCompReflexion.comp Hom.rightCompReflexion)

pp: case reflexion.leftCompReflexion.id
⊢ (Hom.reflexion.comp Hom.leftCompReflexion).comp (Hom.id one) =
    Hom.reflexion.comp (Hom.leftCompReflexion.comp (Hom.id one))

pp: case reflexion.rightCompReflexion.left
⊢ (Hom.reflexion.comp Hom.rightCompReflexion).comp Hom.left = Hom.reflexion.comp (Hom.rightCompReflexion.comp Hom.left)

pp: case reflexion.rightCompReflexion.right
⊢ (Hom.reflexion.comp Hom.rightCompReflexion).comp Hom.right =
    Hom.reflexion.comp (Hom.rightCompReflexion.comp Hom.right)

pp: case reflexion.rightCompReflexion.leftCompReflexion
⊢ (Hom.reflexion.comp Hom.rightCompReflexion).comp Hom.leftCompReflexion =
    Hom.reflexion.comp (Hom.rightCompReflexion.comp Hom.leftCompReflexion)

pp: case reflexion.rightCompReflexion.rightCompReflexion
⊢ (Hom.reflexion.comp Hom.rightCompReflexion).comp Hom.rightCompReflexion =
    Hom.reflexion.comp (Hom.rightCompReflexion.comp Hom.rightCompReflexion)

pp: case reflexion.rightCompReflexion.id
⊢ (Hom.reflexion.comp Hom.rightCompReflexion).comp (Hom.id one) =
    Hom.reflexion.comp (Hom.rightCompReflexion.comp (Hom.id one))

pp: case reflexion.id.left
⊢ (Hom.reflexion.comp (Hom.id one)).comp Hom.left = Hom.reflexion.comp ((Hom.id one).comp Hom.left)

pp: case reflexion.id.right
⊢ (Hom.reflexion.comp (Hom.id one)).comp Hom.right = Hom.reflexion.comp ((Hom.id one).comp Hom.right)

pp: case reflexion.id.leftCompReflexion
⊢ (Hom.reflexion.comp (Hom.id one)).comp Hom.leftCompReflexion =
    Hom.reflexion.comp ((Hom.id one).comp Hom.leftCompReflexion)

pp: case reflexion.id.rightCompReflexion
⊢ (Hom.reflexion.comp (Hom.id one)).comp Hom.rightCompReflexion =
    Hom.reflexion.comp ((Hom.id one).comp Hom.rightCompReflexion)

pp: case reflexion.id.id
⊢ (Hom.reflexion.comp (Hom.id one)).comp (Hom.id one) = Hom.reflexion.comp ((Hom.id one).comp (Hom.id one))

pp: case leftCompReflexion.left.reflexion
⊢ (Hom.leftCompReflexion.comp Hom.left).comp Hom.reflexion = Hom.leftCompReflexion.comp (Hom.left.comp Hom.reflexion)

pp: case leftCompReflexion.left.id
⊢ (Hom.leftCompReflexion.comp Hom.left).comp (Hom.id zero) = Hom.leftCompReflexion.comp (Hom.left.comp (Hom.id zero))

pp: case leftCompReflexion.right.reflexion
⊢ (Hom.leftCompReflexion.comp Hom.right).comp Hom.reflexion = Hom.leftCompReflexion.comp (Hom.right.comp Hom.reflexion)

pp: case leftCompReflexion.right.id
⊢ (Hom.leftCompReflexion.comp Hom.right).comp (Hom.id zero) = Hom.leftCompReflexion.comp (Hom.right.comp (Hom.id zero))

pp: case leftCompReflexion.leftCompReflexion.left
⊢ (Hom.leftCompReflexion.comp Hom.leftCompReflexion).comp Hom.left =
    Hom.leftCompReflexion.comp (Hom.leftCompReflexion.comp Hom.left)

pp: case leftCompReflexion.leftCompReflexion.right
⊢ (Hom.leftCompReflexion.comp Hom.leftCompReflexion).comp Hom.right =
    Hom.leftCompReflexion.comp (Hom.leftCompReflexion.comp Hom.right)

pp: case leftCompReflexion.leftCompReflexion.leftCompReflexion
⊢ (Hom.leftCompReflexion.comp Hom.leftCompReflexion).comp Hom.leftCompReflexion =
    Hom.leftCompReflexion.comp (Hom.leftCompReflexion.comp Hom.leftCompReflexion)

pp: case leftCompReflexion.leftCompReflexion.rightCompReflexion
⊢ (Hom.leftCompReflexion.comp Hom.leftCompReflexion).comp Hom.rightCompReflexion =
    Hom.leftCompReflexion.comp (Hom.leftCompReflexion.comp Hom.rightCompReflexion)

pp: case leftCompReflexion.leftCompReflexion.id
⊢ (Hom.leftCompReflexion.comp Hom.leftCompReflexion).comp (Hom.id one) =
    Hom.leftCompReflexion.comp (Hom.leftCompReflexion.comp (Hom.id one))

pp: case leftCompReflexion.rightCompReflexion.left
⊢ (Hom.leftCompReflexion.comp Hom.rightCompReflexion).comp Hom.left =
    Hom.leftCompReflexion.comp (Hom.rightCompReflexion.comp Hom.left)

pp: case leftCompReflexion.rightCompReflexion.right
⊢ (Hom.leftCompReflexion.comp Hom.rightCompReflexion).comp Hom.right =
    Hom.leftCompReflexion.comp (Hom.rightCompReflexion.comp Hom.right)

pp: case leftCompReflexion.rightCompReflexion.leftCompReflexion
⊢ (Hom.leftCompReflexion.comp Hom.rightCompReflexion).comp Hom.leftCompReflexion =
    Hom.leftCompReflexion.comp (Hom.rightCompReflexion.comp Hom.leftCompReflexion)

pp: case leftCompReflexion.rightCompReflexion.rightCompReflexion
⊢ (Hom.leftCompReflexion.comp Hom.rightCompReflexion).comp Hom.rightCompReflexion =
    Hom.leftCompReflexion.comp (Hom.rightCompReflexion.comp Hom.rightCompReflexion)

pp: case leftCompReflexion.rightCompReflexion.id
⊢ (Hom.leftCompReflexion.comp Hom.rightCompReflexion).comp (Hom.id one) =
    Hom.leftCompReflexion.comp (Hom.rightCompReflexion.comp (Hom.id one))

pp: case leftCompReflexion.id.left
⊢ (Hom.leftCompReflexion.comp (Hom.id one)).comp Hom.left = Hom.leftCompReflexion.comp ((Hom.id one).comp Hom.left)

pp: case leftCompReflexion.id.right
⊢ (Hom.leftCompReflexion.comp (Hom.id one)).comp Hom.right = Hom.leftCompReflexion.comp ((Hom.id one).comp Hom.right)

pp: case leftCompReflexion.id.leftCompReflexion
⊢ (Hom.leftCompReflexion.comp (Hom.id one)).comp Hom.leftCompReflexion =
    Hom.leftCompReflexion.comp ((Hom.id one).comp Hom.leftCompReflexion)

pp: case leftCompReflexion.id.rightCompReflexion
⊢ (Hom.leftCompReflexion.comp (Hom.id one)).comp Hom.rightCompReflexion =
    Hom.leftCompReflexion.comp ((Hom.id one).comp Hom.rightCompReflexion)

pp: case leftCompReflexion.id.id
⊢ (Hom.leftCompReflexion.comp (Hom.id one)).comp (Hom.id one) =
    Hom.leftCompReflexion.comp ((Hom.id one).comp (Hom.id one))

pp: case rightCompReflexion.left.reflexion
⊢ (Hom.rightCompReflexion.comp Hom.left).comp Hom.reflexion = Hom.rightCompReflexion.comp (Hom.left.comp Hom.reflexion)

pp: case rightCompReflexion.left.id
⊢ (Hom.rightCompReflexion.comp Hom.left).comp (Hom.id zero) = Hom.rightCompReflexion.comp (Hom.left.comp (Hom.id zero))

pp: case rightCompReflexion.right.reflexion
⊢ (Hom.rightCompReflexion.comp Hom.right).comp Hom.reflexion =
    Hom.rightCompReflexion.comp (Hom.right.comp Hom.reflexion)

pp: case rightCompReflexion.right.id
⊢ (Hom.rightCompReflexion.comp Hom.right).comp (Hom.id zero) =
    Hom.rightCompReflexion.comp (Hom.right.comp (Hom.id zero))

pp: case rightCompReflexion.leftCompReflexion.left
⊢ (Hom.rightCompReflexion.comp Hom.leftCompReflexion).comp Hom.left =
    Hom.rightCompReflexion.comp (Hom.leftCompReflexion.comp Hom.left)

pp: case rightCompReflexion.leftCompReflexion.right
⊢ (Hom.rightCompReflexion.comp Hom.leftCompReflexion).comp Hom.right =
    Hom.rightCompReflexion.comp (Hom.leftCompReflexion.comp Hom.right)

pp: case rightCompReflexion.leftCompReflexion.leftCompReflexion
⊢ (Hom.rightCompReflexion.comp Hom.leftCompReflexion).comp Hom.leftCompReflexion =
    Hom.rightCompReflexion.comp (Hom.leftCompReflexion.comp Hom.leftCompReflexion)

pp: case rightCompReflexion.leftCompReflexion.rightCompReflexion
⊢ (Hom.rightCompReflexion.comp Hom.leftCompReflexion).comp Hom.rightCompReflexion =
    Hom.rightCompReflexion.comp (Hom.leftCompReflexion.comp Hom.rightCompReflexion)

pp: case rightCompReflexion.leftCompReflexion.id
⊢ (Hom.rightCompReflexion.comp Hom.leftCompReflexion).comp (Hom.id one) =
    Hom.rightCompReflexion.comp (Hom.leftCompReflexion.comp (Hom.id one))

pp: case rightCompReflexion.rightCompReflexion.left
⊢ (Hom.rightCompReflexion.comp Hom.rightCompReflexion).comp Hom.left =
    Hom.rightCompReflexion.comp (Hom.rightCompReflexion.comp Hom.left)

pp: case rightCompReflexion.rightCompReflexion.right
⊢ (Hom.rightCompReflexion.comp Hom.rightCompReflexion).comp Hom.right =
    Hom.rightCompReflexion.comp (Hom.rightCompReflexion.comp Hom.right)

pp: case rightCompReflexion.rightCompReflexion.leftCompReflexion
⊢ (Hom.rightCompReflexion.comp Hom.rightCompReflexion).comp Hom.leftCompReflexion =
    Hom.rightCompReflexion.comp (Hom.rightCompReflexion.comp Hom.leftCompReflexion)

pp: case rightCompReflexion.rightCompReflexion.rightCompReflexion
⊢ (Hom.rightCompReflexion.comp Hom.rightCompReflexion).comp Hom.rightCompReflexion =
    Hom.rightCompReflexion.comp (Hom.rightCompReflexion.comp Hom.rightCompReflexion)

pp: case rightCompReflexion.rightCompReflexion.id
⊢ (Hom.rightCompReflexion.comp Hom.rightCompReflexion).comp (Hom.id one) =
    Hom.rightCompReflexion.comp (Hom.rightCompReflexion.comp (Hom.id one))

pp: case rightCompReflexion.id.left
⊢ (Hom.rightCompReflexion.comp (Hom.id one)).comp Hom.left = Hom.rightCompReflexion.comp ((Hom.id one).comp Hom.left)

pp: case rightCompReflexion.id.right
⊢ (Hom.rightCompReflexion.comp (Hom.id one)).comp Hom.right = Hom.rightCompReflexion.comp ((Hom.id one).comp Hom.right)

pp: case rightCompReflexion.id.leftCompReflexion
⊢ (Hom.rightCompReflexion.comp (Hom.id one)).comp Hom.leftCompReflexion =
    Hom.rightCompReflexion.comp ((Hom.id one).comp Hom.leftCompReflexion)

pp: case rightCompReflexion.id.rightCompReflexion
⊢ (Hom.rightCompReflexion.comp (Hom.id one)).comp Hom.rightCompReflexion =
    Hom.rightCompReflexion.comp ((Hom.id one).comp Hom.rightCompReflexion)

pp: case rightCompReflexion.id.id
⊢ (Hom.rightCompReflexion.comp (Hom.id one)).comp (Hom.id one) =
    Hom.rightCompReflexion.comp ((Hom.id one).comp (Hom.id one))

pp: case id.left.reflexion
⊢ ((Hom.id one).comp Hom.left).comp Hom.reflexion = (Hom.id one).comp (Hom.left.comp Hom.reflexion)

pp: case id.left.id
⊢ ((Hom.id one).comp Hom.left).comp (Hom.id zero) = (Hom.id one).comp (Hom.left.comp (Hom.id zero))

pp: case id.right.reflexion
⊢ ((Hom.id one).comp Hom.right).comp Hom.reflexion = (Hom.id one).comp (Hom.right.comp Hom.reflexion)

pp: case id.right.id
⊢ ((Hom.id one).comp Hom.right).comp (Hom.id zero) = (Hom.id one).comp (Hom.right.comp (Hom.id zero))

pp: case id.reflexion.left
⊢ ((Hom.id zero).comp Hom.reflexion).comp Hom.left = (Hom.id zero).comp (Hom.reflexion.comp Hom.left)

pp: case id.reflexion.right
⊢ ((Hom.id zero).comp Hom.reflexion).comp Hom.right = (Hom.id zero).comp (Hom.reflexion.comp Hom.right)

pp: case id.reflexion.leftCompReflexion
⊢ ((Hom.id zero).comp Hom.reflexion).comp Hom.leftCompReflexion =
    (Hom.id zero).comp (Hom.reflexion.comp Hom.leftCompReflexion)

pp: case id.reflexion.rightCompReflexion
⊢ ((Hom.id zero).comp Hom.reflexion).comp Hom.rightCompReflexion =
    (Hom.id zero).comp (Hom.reflexion.comp Hom.rightCompReflexion)

pp: case id.reflexion.id
⊢ ((Hom.id zero).comp Hom.reflexion).comp (Hom.id one) = (Hom.id zero).comp (Hom.reflexion.comp (Hom.id one))

pp: case id.leftCompReflexion.left
⊢ ((Hom.id one).comp Hom.leftCompReflexion).comp Hom.left = (Hom.id one).comp (Hom.leftCompReflexion.comp Hom.left)

pp: case id.leftCompReflexion.right
⊢ ((Hom.id one).comp Hom.leftCompReflexion).comp Hom.right = (Hom.id one).comp (Hom.leftCompReflexion.comp Hom.right)

pp: case id.leftCompReflexion.leftCompReflexion
⊢ ((Hom.id one).comp Hom.leftCompReflexion).comp Hom.leftCompReflexion =
    (Hom.id one).comp (Hom.leftCompReflexion.comp Hom.leftCompReflexion)

pp: case id.leftCompReflexion.rightCompReflexion
⊢ ((Hom.id one).comp Hom.leftCompReflexion).comp Hom.rightCompReflexion =
    (Hom.id one).comp (Hom.leftCompReflexion.comp Hom.rightCompReflexion)

pp: case id.leftCompReflexion.id
⊢ ((Hom.id one).comp Hom.leftCompReflexion).comp (Hom.id one) =
    (Hom.id one).comp (Hom.leftCompReflexion.comp (Hom.id one))

pp: case id.rightCompReflexion.left
⊢ ((Hom.id one).comp Hom.rightCompReflexion).comp Hom.left = (Hom.id one).comp (Hom.rightCompReflexion.comp Hom.left)

pp: case id.rightCompReflexion.right
⊢ ((Hom.id one).comp Hom.rightCompReflexion).comp Hom.right = (Hom.id one).comp (Hom.rightCompReflexion.comp Hom.right)

pp: case id.rightCompReflexion.leftCompReflexion
⊢ ((Hom.id one).comp Hom.rightCompReflexion).comp Hom.leftCompReflexion =
    (Hom.id one).comp (Hom.rightCompReflexion.comp Hom.leftCompReflexion)

pp: case id.rightCompReflexion.rightCompReflexion
⊢ ((Hom.id one).comp Hom.rightCompReflexion).comp Hom.rightCompReflexion =
    (Hom.id one).comp (Hom.rightCompReflexion.comp Hom.rightCompReflexion)

pp: case id.rightCompReflexion.id
⊢ ((Hom.id one).comp Hom.rightCompReflexion).comp (Hom.id one) =
    (Hom.id one).comp (Hom.rightCompReflexion.comp (Hom.id one))

pp: case id.id.left
⊢ ((Hom.id one).comp (Hom.id one)).comp Hom.left = (Hom.id one).comp ((Hom.id one).comp Hom.left)

pp: case id.id.right
⊢ ((Hom.id one).comp (Hom.id one)).comp Hom.right = (Hom.id one).comp ((Hom.id one).comp Hom.right)

pp: case id.id.reflexion
⊢ ((Hom.id zero).comp (Hom.id zero)).comp Hom.reflexion = (Hom.id zero).comp ((Hom.id zero).comp Hom.reflexion)

pp: case id.id.leftCompReflexion
⊢ ((Hom.id one).comp (Hom.id one)).comp Hom.leftCompReflexion =
    (Hom.id one).comp ((Hom.id one).comp Hom.leftCompReflexion)

pp: case id.id.rightCompReflexion
⊢ ((Hom.id one).comp (Hom.id one)).comp Hom.rightCompReflexion =
    (Hom.id one).comp ((Hom.id one).comp Hom.rightCompReflexion)

pp: case id.id.id
W✝ : WalkingReflexivePair
⊢ ((Hom.id W✝).comp (Hom.id W✝)).comp (Hom.id W✝) = (Hom.id W✝).comp ((Hom.id W✝).comp (Hom.id W✝))

Tactic:
<;>

Goal state after:
case left.reflexion.left
⊢ (Hom.left.comp Hom.reflexion).comp Hom.left = Hom.left.comp (Hom.reflexion.comp Hom.left)

case left.reflexion.right
⊢ (Hom.left.comp Hom.reflexion).comp Hom.right = Hom.left.comp (Hom.reflexion.comp Hom.right)

case left.reflexion.leftCompReflexion
⊢ (Hom.left.comp Hom.reflexion).comp Hom.leftCompReflexion = Hom.left.comp (Hom.reflexion.comp Hom.leftCompReflexion)

case left.reflexion.rightCompReflexion
⊢ (Hom.left.comp Hom.reflexion).comp Hom.rightCompReflexion = Hom.left.comp (Hom.reflexion.comp Hom.rightCompReflexion)

case left.reflexion.id
⊢ (Hom.left.comp Hom.reflexion).comp (Hom.id one) = Hom.left.comp (Hom.reflexion.comp (Hom.id one))

case left.id.reflexion
⊢ (Hom.left.comp (Hom.id zero)).comp Hom.reflexion = Hom.left.comp ((Hom.id zero).comp Hom.reflexion)

case left.id.id
⊢ (Hom.left.comp (Hom.id zero)).comp (Hom.id zero) = Hom.left.comp ((Hom.id zero).comp (Hom.id zero))

case right.reflexion.left
⊢ (Hom.right.comp Hom.reflexion).comp Hom.left = Hom.right.comp (Hom.reflexion.comp Hom.left)

case right.reflexion.right
⊢ (Hom.right.comp Hom.reflexion).comp Hom.right = Hom.right.comp (Hom.reflexion.comp Hom.right)

case right.reflexion.leftCompReflexion
⊢ (Hom.right.comp Hom.reflexion).comp Hom.leftCompReflexion = Hom.right.comp (Hom.reflexion.comp Hom.leftCompReflexion)

case right.reflexion.rightCompReflexion
⊢ (Hom.right.comp Hom.reflexion).comp Hom.rightCompReflexion =
    Hom.right.comp (Hom.reflexion.comp Hom.rightCompReflexion)

case right.reflexion.id
⊢ (Hom.right.comp Hom.reflexion).comp (Hom.id one) = Hom.right.comp (Hom.reflexion.comp (Hom.id one))

case right.id.reflexion
⊢ (Hom.right.comp (Hom.id zero)).comp Hom.reflexion = Hom.right.comp ((Hom.id zero).comp Hom.reflexion)

case right.id.id
⊢ (Hom.right.comp (Hom.id zero)).comp (Hom.id zero) = Hom.right.comp ((Hom.id zero).comp (Hom.id zero))

case reflexion.left.reflexion
⊢ (Hom.reflexion.comp Hom.left).comp Hom.reflexion = Hom.reflexion.comp (Hom.left.comp Hom.reflexion)

case reflexion.left.id
⊢ (Hom.reflexion.comp Hom.left).comp (Hom.id zero) = Hom.reflexion.comp (Hom.left.comp (Hom.id zero))

case reflexion.right.reflexion
⊢ (Hom.reflexion.comp Hom.right).comp Hom.reflexion = Hom.reflexion.comp (Hom.right.comp Hom.reflexion)

case reflexion.right.id
⊢ (Hom.reflexion.comp Hom.right).comp (Hom.id zero) = Hom.reflexion.comp (Hom.right.comp (Hom.id zero))

case reflexion.leftCompReflexion.left
⊢ (Hom.reflexion.comp Hom.leftCompReflexion).comp Hom.left = Hom.reflexion.comp (Hom.leftCompReflexion.comp Hom.left)

case reflexion.leftCompReflexion.right
⊢ (Hom.reflexion.comp Hom.leftCompReflexion).comp Hom.right = Hom.reflexion.comp (Hom.leftCompReflexion.comp Hom.right)

case reflexion.leftCompReflexion.leftCompReflexion
⊢ (Hom.reflexion.comp Hom.leftCompReflexion).comp Hom.leftCompReflexion =
    Hom.reflexion.comp (Hom.leftCompReflexion.comp Hom.leftCompReflexion)

case reflexion.leftCompReflexion.rightCompReflexion
⊢ (Hom.reflexion.comp Hom.leftCompReflexion).comp Hom.rightCompReflexion =
    Hom.reflexion.comp (Hom.leftCompReflexion.comp Hom.rightCompReflexion)

case reflexion.leftCompReflexion.id
⊢ (Hom.reflexion.comp Hom.leftCompReflexion).comp (Hom.id one) =
    Hom.reflexion.comp (Hom.leftCompReflexion.comp (Hom.id one))

case reflexion.rightCompReflexion.left
⊢ (Hom.reflexion.comp Hom.rightCompReflexion).comp Hom.left = Hom.reflexion.comp (Hom.rightCompReflexion.comp Hom.left)

case reflexion.rightCompReflexion.right
⊢ (Hom.reflexion.comp Hom.rightCompReflexion).comp Hom.right =
    Hom.reflexion.comp (Hom.rightCompReflexion.comp Hom.right)

case reflexion.rightCompReflexion.leftCompReflexion
⊢ (Hom.reflexion.comp Hom.rightCompReflexion).comp Hom.leftCompReflexion =
    Hom.reflexion.comp (Hom.rightCompReflexion.comp Hom.leftCompReflexion)

case reflexion.rightCompReflexion.rightCompReflexion
⊢ (Hom.reflexion.comp Hom.rightCompReflexion).comp Hom.rightCompReflexion =
    Hom.reflexion.comp (Hom.rightCompReflexion.comp Hom.rightCompReflexion)

case reflexion.rightCompReflexion.id
⊢ (Hom.reflexion.comp Hom.rightCompReflexion).comp (Hom.id one) =
    Hom.reflexion.comp (Hom.rightCompReflexion.comp (Hom.id one))

case reflexion.id.left
⊢ (Hom.reflexion.comp (Hom.id one)).comp Hom.left = Hom.reflexion.comp ((Hom.id one).comp Hom.left)

case reflexion.id.right
⊢ (Hom.reflexion.comp (Hom.id one)).comp Hom.right = Hom.reflexion.comp ((Hom.id one).comp Hom.right)

case reflexion.id.leftCompReflexion
⊢ (Hom.reflexion.comp (Hom.id one)).comp Hom.leftCompReflexion =
    Hom.reflexion.comp ((Hom.id one).comp Hom.leftCompReflexion)

case reflexion.id.rightCompReflexion
⊢ (Hom.reflexion.comp (Hom.id one)).comp Hom.rightCompReflexion =
    Hom.reflexion.comp ((Hom.id one).comp Hom.rightCompReflexion)

case reflexion.id.id
⊢ (Hom.reflexion.comp (Hom.id one)).comp (Hom.id one) = Hom.reflexion.comp ((Hom.id one).comp (Hom.id one))

case leftCompReflexion.left.reflexion
⊢ (Hom.leftCompReflexion.comp Hom.left).comp Hom.reflexion = Hom.leftCompReflexion.comp (Hom.left.comp Hom.reflexion)

case leftCompReflexion.left.id
⊢ (Hom.leftCompReflexion.comp Hom.left).comp (Hom.id zero) = Hom.leftCompReflexion.comp (Hom.left.comp (Hom.id zero))

case leftCompReflexion.right.reflexion
⊢ (Hom.leftCompReflexion.comp Hom.right).comp Hom.reflexion = Hom.leftCompReflexion.comp (Hom.right.comp Hom.reflexion)

case leftCompReflexion.right.id
⊢ (Hom.leftCompReflexion.comp Hom.right).comp (Hom.id zero) = Hom.leftCompReflexion.comp (Hom.right.comp (Hom.id zero))

case leftCompReflexion.leftCompReflexion.left
⊢ (Hom.leftCompReflexion.comp Hom.leftCompReflexion).comp Hom.left =
    Hom.leftCompReflexion.comp (Hom.leftCompReflexion.comp Hom.left)

case leftCompReflexion.leftCompReflexion.right
⊢ (Hom.leftCompReflexion.comp Hom.leftCompReflexion).comp Hom.right =
    Hom.leftCompReflexion.comp (Hom.leftCompReflexion.comp Hom.right)

case leftCompReflexion.leftCompReflexion.leftCompReflexion
⊢ (Hom.leftCompReflexion.comp Hom.leftCompReflexion).comp Hom.leftCompReflexion =
    Hom.leftCompReflexion.comp (Hom.leftCompReflexion.comp Hom.leftCompReflexion)

case leftCompReflexion.leftCompReflexion.rightCompReflexion
⊢ (Hom.leftCompReflexion.comp Hom.leftCompReflexion).comp Hom.rightCompReflexion =
    Hom.leftCompReflexion.comp (Hom.leftCompReflexion.comp Hom.rightCompReflexion)

case leftCompReflexion.leftCompReflexion.id
⊢ (Hom.leftCompReflexion.comp Hom.leftCompReflexion).comp (Hom.id one) =
    Hom.leftCompReflexion.comp (Hom.leftCompReflexion.comp (Hom.id one))

case leftCompReflexion.rightCompReflexion.left
⊢ (Hom.leftCompReflexion.comp Hom.rightCompReflexion).comp Hom.left =
    Hom.leftCompReflexion.comp (Hom.rightCompReflexion.comp Hom.left)

case leftCompReflexion.rightCompReflexion.right
⊢ (Hom.leftCompReflexion.comp Hom.rightCompReflexion).comp Hom.right =
    Hom.leftCompReflexion.comp (Hom.rightCompReflexion.comp Hom.right)

case leftCompReflexion.rightCompReflexion.leftCompReflexion
⊢ (Hom.leftCompReflexion.comp Hom.rightCompReflexion).comp Hom.leftCompReflexion =
    Hom.leftCompReflexion.comp (Hom.rightCompReflexion.comp Hom.leftCompReflexion)

case leftCompReflexion.rightCompReflexion.rightCompReflexion
⊢ (Hom.leftCompReflexion.comp Hom.rightCompReflexion).comp Hom.rightCompReflexion =
    Hom.leftCompReflexion.comp (Hom.rightCompReflexion.comp Hom.rightCompReflexion)

case leftCompReflexion.rightCompReflexion.id
⊢ (Hom.leftCompReflexion.comp Hom.rightCompReflexion).comp (Hom.id one) =
    Hom.leftCompReflexion.comp (Hom.rightCompReflexion.comp (Hom.id one))

case leftCompReflexion.id.left
⊢ (Hom.leftCompReflexion.comp (Hom.id one)).comp Hom.left = Hom.leftCompReflexion.comp ((Hom.id one).comp Hom.left)

case leftCompReflexion.id.right
⊢ (Hom.leftCompReflexion.comp (Hom.id one)).comp Hom.right = Hom.leftCompReflexion.comp ((Hom.id one).comp Hom.right)

case leftCompReflexion.id.leftCompReflexion
⊢ (Hom.leftCompReflexion.comp (Hom.id one)).comp Hom.leftCompReflexion =
    Hom.leftCompReflexion.comp ((Hom.id one).comp Hom.leftCompReflexion)

case leftCompReflexion.id.rightCompReflexion
⊢ (Hom.leftCompReflexion.comp (Hom.id one)).comp Hom.rightCompReflexion =
    Hom.leftCompReflexion.comp ((Hom.id one).comp Hom.rightCompReflexion)

case leftCompReflexion.id.id
⊢ (Hom.leftCompReflexion.comp (Hom.id one)).comp (Hom.id one) =
    Hom.leftCompReflexion.comp ((Hom.id one).comp (Hom.id one))

case rightCompReflexion.left.reflexion
⊢ (Hom.rightCompReflexion.comp Hom.left).comp Hom.reflexion = Hom.rightCompReflexion.comp (Hom.left.comp Hom.reflexion)

case rightCompReflexion.left.id
⊢ (Hom.rightCompReflexion.comp Hom.left).comp (Hom.id zero) = Hom.rightCompReflexion.comp (Hom.left.comp (Hom.id zero))

case rightCompReflexion.right.reflexion
⊢ (Hom.rightCompReflexion.comp Hom.right).comp Hom.reflexion =
    Hom.rightCompReflexion.comp (Hom.right.comp Hom.reflexion)

case rightCompReflexion.right.id
⊢ (Hom.rightCompReflexion.comp Hom.right).comp (Hom.id zero) =
    Hom.rightCompReflexion.comp (Hom.right.comp (Hom.id zero))

case rightCompReflexion.leftCompReflexion.left
⊢ (Hom.rightCompReflexion.comp Hom.leftCompReflexion).comp Hom.left =
    Hom.rightCompReflexion.comp (Hom.leftCompReflexion.comp Hom.left)

case rightCompReflexion.leftCompReflexion.right
⊢ (Hom.rightCompReflexion.comp Hom.leftCompReflexion).comp Hom.right =
    Hom.rightCompReflexion.comp (Hom.leftCompReflexion.comp Hom.right)

case rightCompReflexion.leftCompReflexion.leftCompReflexion
⊢ (Hom.rightCompReflexion.comp Hom.leftCompReflexion).comp Hom.leftCompReflexion =
    Hom.rightCompReflexion.comp (Hom.leftCompReflexion.comp Hom.leftCompReflexion)

case rightCompReflexion.leftCompReflexion.rightCompReflexion
⊢ (Hom.rightCompReflexion.comp Hom.leftCompReflexion).comp Hom.rightCompReflexion =
    Hom.rightCompReflexion.comp (Hom.leftCompReflexion.comp Hom.rightCompReflexion)

case rightCompReflexion.leftCompReflexion.id
⊢ (Hom.rightCompReflexion.comp Hom.leftCompReflexion).comp (Hom.id one) =
    Hom.rightCompReflexion.comp (Hom.leftCompReflexion.comp (Hom.id one))

case rightCompReflexion.rightCompReflexion.left
⊢ (Hom.rightCompReflexion.comp Hom.rightCompReflexion).comp Hom.left =
    Hom.rightCompReflexion.comp (Hom.rightCompReflexion.comp Hom.left)

case rightCompReflexion.rightCompReflexion.right
⊢ (Hom.rightCompReflexion.comp Hom.rightCompReflexion).comp Hom.right =
    Hom.rightCompReflexion.comp (Hom.rightCompReflexion.comp Hom.right)

case rightCompReflexion.rightCompReflexion.leftCompReflexion
⊢ (Hom.rightCompReflexion.comp Hom.rightCompReflexion).comp Hom.leftCompReflexion =
    Hom.rightCompReflexion.comp (Hom.rightCompReflexion.comp Hom.leftCompReflexion)

case rightCompReflexion.rightCompReflexion.rightCompReflexion
⊢ (Hom.rightCompReflexion.comp Hom.rightCompReflexion).comp Hom.rightCompReflexion =
    Hom.rightCompReflexion.comp (Hom.rightCompReflexion.comp Hom.rightCompReflexion)

case rightCompReflexion.rightCompReflexion.id
⊢ (Hom.rightCompReflexion.comp Hom.rightCompReflexion).comp (Hom.id one) =
    Hom.rightCompReflexion.comp (Hom.rightCompReflexion.comp (Hom.id one))

case rightCompReflexion.id.left
⊢ (Hom.rightCompReflexion.comp (Hom.id one)).comp Hom.left = Hom.rightCompReflexion.comp ((Hom.id one).comp Hom.left)

case rightCompReflexion.id.right
⊢ (Hom.rightCompReflexion.comp (Hom.id one)).comp Hom.right = Hom.rightCompReflexion.comp ((Hom.id one).comp Hom.right)

case rightCompReflexion.id.leftCompReflexion
⊢ (Hom.rightCompReflexion.comp (Hom.id one)).comp Hom.leftCompReflexion =
    Hom.rightCompReflexion.comp ((Hom.id one).comp Hom.leftCompReflexion)

case rightCompReflexion.id.rightCompReflexion
⊢ (Hom.rightCompReflexion.comp (Hom.id one)).comp Hom.rightCompReflexion =
    Hom.rightCompReflexion.comp ((Hom.id one).comp Hom.rightCompReflexion)

case rightCompReflexion.id.id
⊢ (Hom.rightCompReflexion.comp (Hom.id one)).comp (Hom.id one) =
    Hom.rightCompReflexion.comp ((Hom.id one).comp (Hom.id one))

case id.left.reflexion
⊢ ((Hom.id one).comp Hom.left).comp Hom.reflexion = (Hom.id one).comp (Hom.left.comp Hom.reflexion)

case id.left.id
⊢ ((Hom.id one).comp Hom.left).comp (Hom.id zero) = (Hom.id one).comp (Hom.left.comp (Hom.id zero))

case id.right.reflexion
⊢ ((Hom.id one).comp Hom.right).comp Hom.reflexion = (Hom.id one).comp (Hom.right.comp Hom.reflexion)

case id.right.id
⊢ ((Hom.id one).comp Hom.right).comp (Hom.id zero) = (Hom.id one).comp (Hom.right.comp (Hom.id zero))

case id.reflexion.left
⊢ ((Hom.id zero).comp Hom.reflexion).comp Hom.left = (Hom.id zero).comp (Hom.reflexion.comp Hom.left)

case id.reflexion.right
⊢ ((Hom.id zero).comp Hom.reflexion).comp Hom.right = (Hom.id zero).comp (Hom.reflexion.comp Hom.right)

case id.reflexion.leftCompReflexion
⊢ ((Hom.id zero).comp Hom.reflexion).comp Hom.leftCompReflexion =
    (Hom.id zero).comp (Hom.reflexion.comp Hom.leftCompReflexion)

case id.reflexion.rightCompReflexion
⊢ ((Hom.id zero).comp Hom.reflexion).comp Hom.rightCompReflexion =
    (Hom.id zero).comp (Hom.reflexion.comp Hom.rightCompReflexion)

case id.reflexion.id
⊢ ((Hom.id zero).comp Hom.reflexion).comp (Hom.id one) = (Hom.id zero).comp (Hom.reflexion.comp (Hom.id one))

case id.leftCompReflexion.left
⊢ ((Hom.id one).comp Hom.leftCompReflexion).comp Hom.left = (Hom.id one).comp (Hom.leftCompReflexion.comp Hom.left)

case id.leftCompReflexion.right
⊢ ((Hom.id one).comp Hom.leftCompReflexion).comp Hom.right = (Hom.id one).comp (Hom.leftCompReflexion.comp Hom.right)

case id.leftCompReflexion.leftCompReflexion
⊢ ((Hom.id one).comp Hom.leftCompReflexion).comp Hom.leftCompReflexion =
    (Hom.id one).comp (Hom.leftCompReflexion.comp Hom.leftCompReflexion)

case id.leftCompReflexion.rightCompReflexion
⊢ ((Hom.id one).comp Hom.leftCompReflexion).comp Hom.rightCompReflexion =
    (Hom.id one).comp (Hom.leftCompReflexion.comp Hom.rightCompReflexion)

case id.leftCompReflexion.id
⊢ ((Hom.id one).comp Hom.leftCompReflexion).comp (Hom.id one) =
    (Hom.id one).comp (Hom.leftCompReflexion.comp (Hom.id one))

case id.rightCompReflexion.left
⊢ ((Hom.id one).comp Hom.rightCompReflexion).comp Hom.left = (Hom.id one).comp (Hom.rightCompReflexion.comp Hom.left)

case id.rightCompReflexion.right
⊢ ((Hom.id one).comp Hom.rightCompReflexion).comp Hom.right = (Hom.id one).comp (Hom.rightCompReflexion.comp Hom.right)

case id.rightCompReflexion.leftCompReflexion
⊢ ((Hom.id one).comp Hom.rightCompReflexion).comp Hom.leftCompReflexion =
    (Hom.id one).comp (Hom.rightCompReflexion.comp Hom.leftCompReflexion)

case id.rightCompReflexion.rightCompReflexion
⊢ ((Hom.id one).comp Hom.rightCompReflexion).comp Hom.rightCompReflexion =
    (Hom.id one).comp (Hom.rightCompReflexion.comp Hom.rightCompReflexion)

case id.rightCompReflexion.id
⊢ ((Hom.id one).comp Hom.rightCompReflexion).comp (Hom.id one) =
    (Hom.id one).comp (Hom.rightCompReflexion.comp (Hom.id one))

case id.id.left
⊢ ((Hom.id one).comp (Hom.id one)).comp Hom.left = (Hom.id one).comp ((Hom.id one).comp Hom.left)

case id.id.right
⊢ ((Hom.id one).comp (Hom.id one)).comp Hom.right = (Hom.id one).comp ((Hom.id one).comp Hom.right)

case id.id.reflexion
⊢ ((Hom.id zero).comp (Hom.id zero)).comp Hom.reflexion = (Hom.id zero).comp ((Hom.id zero).comp Hom.reflexion)

case id.id.leftCompReflexion
⊢ ((Hom.id one).comp (Hom.id one)).comp Hom.leftCompReflexion =
    (Hom.id one).comp ((Hom.id one).comp Hom.leftCompReflexion)

case id.id.rightCompReflexion
⊢ ((Hom.id one).comp (Hom.id one)).comp Hom.rightCompReflexion =
    (Hom.id one).comp ((Hom.id one).comp Hom.rightCompReflexion)

case id.id.id
W✝ : WalkingReflexivePair
⊢ ((Hom.id W✝).comp (Hom.id W✝)).comp (Hom.id W✝) = (Hom.id W✝).comp ((Hom.id W✝).comp (Hom.id W✝))