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