# (prove_monotonicity_hyps o derive_nonschematic_inductive_relations)
`even(0) /\ odd(1) /\
(!n. even(n) ==> odd(n + 1)) /\ (!n. odd(n) ==> even(n + 1))`;;
val it : thm =
odd =
(\a0. !odd' even'.
(!a0. a0 = 1 \/ (?n. a0 = n + 1 /\ even' n) ==> odd' a0) /\
(!a1. a1 = 0 \/ (?n. a1 = n + 1 /\ odd' n) ==> even' a1)
==> odd' a0),
even =
(\a1. !odd' even'.
(!a0. a0 = 1 \/ (?n. a0 = n + 1 /\ even' n) ==> odd' a0) /\
(!a1. a1 = 0 \/ (?n. a1 = n + 1 /\ odd' n) ==> even' a1)
==> even' a1)
|- (even 0 /\
odd 1 /\
(!n. even n ==> odd (n + 1)) /\
(!n. odd n ==> even (n + 1))) /\
(!odd' even'.
even' 0 /\
odd' 1 /\
(!n. even' n ==> odd' (n + 1)) /\
(!n. odd' n ==> even' (n + 1))
==> (!a0. odd a0 ==> odd' a0) /\ (!a1. even a1 ==> even' a1)) /\
(!a0. odd a0 <=> a0 = 1 \/ (?n. a0 = n + 1 /\ even n)) /\
(!a1. even a1 <=> a1 = 0 \/ (?n. a1 = n + 1 /\ odd n))

Note that the final theorem has two assumptions that one can think of
as the appropriate explicit definitions of these relations, and the conclusion
gives the rule, induction and cases theorems.