Typo fixes and proof fixes

[Pi-Cla]

• Changed "anti-reflexive" to "irreflexive" as anti-reflexivity was never introduced in this book, instead irreflexivity was.
• f(n)=g(n-1) as g: Nat-> A , and f: posInt -> A, so now if n=1, f(1)=g(0).
• Regarding the proof for proposition 4.21, its composition should have been the other way around so now the domains and co-domains should match up. Also, f and g seemed to get mixed up near the end as well. Such as referencing x\in A such that g(x) even though g: posInt -> A.

[rzach]

Thanks!