cases b
case mk
b c : ℤθ
f✝ g✝ h✝ : ℤ
⊢ add (add { f := f✝, g := g✝, h := h✝ } b) c = add { f := f✝, g := g✝, h := h✝ } (add b c)
case mk.mk
c : ℤθ
f✝¹ g✝¹ h✝¹ f✝ g✝ h✝ : ℤ
⊢ add (add { f := f✝¹, g := g✝¹, h := h✝¹ } { f := f✝, g := g✝, h := h✝ }) c =
    add { f := f✝¹, g := g✝¹, h := h✝¹ } (add { f := f✝, g := g✝, h := h✝ } c)