Exercise 11.5 Create a certified book (see certify-book) that starts with definitions including the definition of perm, concludes with (defequiv perm), and has any number of local events in between. We suggest proceeding as follows. - Prove (perm xx ). - Prove (implies (perm xy ) (perm yx) ). - Prove (implies (and (perm x y) (perm yz ) (perm xz) ). - Use :trans1 to print out the immediate expansion - Prove (defeguiv perm). We will use the fact that perm is an equivalence relation by proving some congruence rules. We use the macro defcong to prove congruence rules