Writing a function to find the head of each item in list of lists

Using Rocq
9

First you cannot imagine have a hd function from list A to A for an arbitrary A. This is why you need a default argument in the definition of hd. This leads to hd : A -> list A -> A.
Then in your code for maphd, the term hd a should be hd default a : A for some appropriate default element of type A. So the most direct modification of your maphd would be:

Fixpoint maphd (default : A) (l: list (list A)) : (list A):=
match l with
  | nil => nil
  | a :: t  => (hd default a):: (maphd default t)
end.

which leads to maphd default [ [] ] = [ default ].

Now if you want maphd to throw away empty lists, you have to say so in the code:

Fixpoint maphd (l: list (list A)) : (list A):=
match l with
  | nil => nil
  | nil :: t => maphd t
  | (a :: r) :: t  => (hd  a (a::r)):: (maphd t)
end.

(here choosing a as default argument) but then the call to hd can be inlined to get:

Fixpoint maphd (l: list (list A)) : (list A):=
match l with
  | nil => nil
  | nil :: t => maphd t
  | (a :: r) :: t  => a :: (maphd t)
end.