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.
Oh, you mean "h(f(a)) and h(g(b)) are defined for all a:A and b:B _and_ that".  I parsed what you wrote as "defined for (all a:A and b:B such that ...)".