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
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
Equality is also one of the most important concept in type theory, which still carries some mysteries remain to be solved.