λ(a : *) → λ(f : a → ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool) → λ(xs : ∀(List : *) → ∀(Cons : ∀(head : a) → ∀(tail : List) → List) → ∀(Nil : List) → List) → xs (∀(Maybe : *) → ∀(Just : ∀(_Just : a) → Maybe) → ∀(Nothing : Maybe) → Maybe) (λ(head : a) → f head (∀(Maybe : *) → ∀(Just : ∀(_Just : a) → Maybe) → ∀(Nothing : Maybe) → Maybe) (λ(Maybe : *) → λ(Just : ∀(_Just : a) → Maybe) → λ(Nothing : Maybe) → Just head)) (λ(Maybe : *) → λ(Just : ∀(_Just : a) → Maybe) → λ(Nothing : Maybe) → Nothing)