Equal Utilities

In the chapter Proving Theorems About Nat, we used some helper functions about Equal, to prove the commutative property of addition for natural number.
The usage of these helper functions are very intuitive, because we are very familiar with reasoning about equations.
And the definition of these helper functions can also be intuitive, once we understood a built-in function called replace.
It expresses a common sense,
If two things are the same, they can replace each other.
Written these helper functions definitely helped us understand the natural of Equal better.
Equality is also one of the most important concept in type theory, which still carries some mysteries remain to be solved.