(*#* Here we define the predicates [even] and [odd] by mutual induction
and we prove the decidability and the exclusion of those predicates.
(*#* Here we define the predicates [even] and [odd] by mutual induction
and we prove the decidability and the exclusion of those predicates.