Change the induction principle of V

This is the fix proposed in issue #699, @spitters and I checked that it is sufficient to prove the rest of the section.
Not really, I mean that we assume two functions of types "forall a, P(f(a))" and "forall b, P(h(b))", and moreover those functions satisfy the condition.
In pattern matching language this says that "h(f(a)) and h(g(b)) are defined for all a and b", such that they moreover satisfy the condition (the first item says the same thing actually, but uses the word "given", maybe we could use the same word to be coherent)