-- BEGINWAIT
-- ENDWAIT
-- BEGININFO
-- SYMBOL|7|15
=
-- ACK
-- TYPE|7|17
ℕ
-- ACK
-- IDENTIFIER|7|17
a
-- ACK
-- TYPE|7|19
ℕ → ℕ → ℕ
-- ACK
-- SYMBOL|7|19
+
-- ACK
-- TYPE|7|21
ℕ
-- ACK
-- IDENTIFIER|7|21
c
-- ACK
-- TYPE|7|23
ℕ → ℕ → ℕ
-- ACK
-- SYMBOL|7|23
+
-- ACK
-- TYPE|7|25
ℕ
-- ACK
-- IDENTIFIER|7|25
b
-- ACK
-- SYMBOL|7|31
by
-- ACK
-- SYMBOL|7|34
rewrite
-- ACK
-- TYPE|7|42
∀ a_1 b_1 c_1, (:a_1 + b_1 + c_1:) = (:a_1 + (b_1 + c_1):)
-- ACK
-- IDENTIFIER|7|42
add.assoc
-- ACK
-- ENDINFO