Replace references to "Martin-L\"{o}f Rule" by "two-sided induction principle for
identity types" and "Paulin-Mohring Rule" by "one-sided induction principle for identity types".