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