- {|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)