∀(Even : *) → ∀(Odd : *) → ∀(Zero : Even) → ∀(SuccE : ∀(pred : Odd) → Even) → ∀(SuccO : ∀(pred : Even) → Odd) → Even