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