cases c
case mk.mk
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ mul { x := x✝¹, y := y✝¹ } (add { x := x✝, y := y✝ } c) =
    add (mul { x := x✝¹, y := y✝¹ } { x := x✝, y := y✝ }) (mul { x := x✝¹, y := y✝¹ } c)
case mk.mk.mk
x✝² y✝² x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ mul { x := x✝², y := y✝² } (add { x := x✝¹, y := y✝¹ } { x := x✝, y := y✝ }) =
    add (mul { x := x✝², y := y✝² } { x := x✝¹, y := y✝¹ }) (mul { x := x✝², y := y✝² } { x := x✝, y := y✝ })