data Empty : * ⇒ {}

absurd [A : *] [x : Empty] : A ⇒ (
  Empty-Elim x (λ _ ⇒ A)
)

record Unit : * ⇒ tt {}

data Nat : * ⇒ { zero : Nat | suc : Nat → Nat }

data List : [A : *] → * ⇒
  { nil : List A | cons : A → List A → List A }

nonEmpty [A : *] [l : List A] : * ⇒ (
   {| h1 |}
)

nonEmpty [A : *] [l : List A] : * ⇒ (
  List-Elim l (λ _ ⇒ *) {|h1|} {|h2|}
)

nonEmpty [A : *] [l : List A] : * ⇒ (
  List-Elim l (λ _ ⇒ *) Empty (λ _ _ _ ⇒ Unit)
)

head [A : *] [l : List A] : nonEmpty A l → A ⇒ (
  List-Elim l (λ l ⇒ nonEmpty A l → A)
    {|h1|} {|h2|}
)

head [A : *] [l : List A] : nonEmpty A l → A ⇒ (
  List-Elim l (λ l ⇒ nonEmpty A l → A)
   (λ p ⇒ {|h1 p|})
   (λ x l pl pxl ⇒ {|h2 x l pl pxl|})
)

head [A : *] [l : List A] : nonEmpty A l → A ⇒ (
  List-Elim l (λ l ⇒ nonEmpty A l → A)
    (λ p ⇒ absurd A p)
    (λ x l pl pxl ⇒ x)
)