Fix ind(D,d,x,y,p) in (i), (ii) and (iii) of Lemma 2.1.4

ind(D,d) : \Pi_{x,y : A} \Pi_{p : x = y} D(x,y,p) according to
Section 1.12.1 (Path induction).
Correction in proof of Thm 4.9.4
Errata for 2c194835, unmarked
Merge pull request #697 from TimRichter/proof494

Proof494
first-order fix to the induction principle of V
unmarked errata for 6d9722d
correct merge marker so Travis can update it
Mark Errata (auto)
Merge pull request #693 from ahorn/lemma-2.1.4

Fix ind(D,d,x,y,p) in (i), (ii) and (iii) of Lemma 2.1.4
Merge pull request #698 from mikeshulman/Vind

first-order fix to the induction principle of V
Mark Errata (auto)
Include (A,a_0) in the statement of Theorem 5.8.2.
remark that 5.8.2(iv) doesn't refer to a_0 or r_0.
Merge pull request #700 from mikeshulman/ppred

Comments on 5.8.2 from Martin Escardo
Errata for #693
Merge branch 'implicitarguments'
Update formal.tex

Typo
Merge pull request #709 from spearman/patch-1

Fix typo in appendix
Updated some Punctuation problems.

In English Punctuation is important for your texts, because when I see a post which have a Punctuation problem, I will never read it, and most of the people will ignore it. It's the psychology of human.

You should put comma before which
it's utility instead of utlity
Punctuation is important in the text.

Punctuation is important in the text.

I fixed 2 Punctuation problems.