Simplify type of D in proof that path induction implies based path induction

In the proof in section 1.12.2 that path induction implies based path induction, the definition of D can be simplified, because the type of C need not depend on "p : x = z". Changing to a non-dependent version matches the premise of based PI better and avoids confusion, since currently p occurs both free and bound in the definition of D.